Generate Typeable info at definition sites
[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, mkWpLams, mkWpLet, mkWpCast,
10 mkWpFun, idHsWrapper, isIdHsWrapper, pprHsWrapper,
11
12 -- Evidence bindings
13 TcEvBinds(..), EvBindsVar(..),
14 EvBindMap(..), emptyEvBindMap, extendEvBinds,
15 lookupEvBind, evBindMapBinds, foldEvBindMap,
16 EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
17 EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors,
18 EvLit(..), evTermCoercion,
19 EvCallStack(..),
20 EvTypeable(..),
21
22 -- TcCoercion
23 TcCoercion(..), TcCoercionR, TcCoercionN,
24 LeftOrRight(..), pickLR,
25 mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo,
26 mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,
27 mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
28 mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo,
29 tcDowngradeRole, mkTcTransAppCo,
30 mkTcAxiomRuleCo, mkTcPhantomCo,
31 tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo,
32 isTcReflCo, getTcCoVar_maybe,
33 tcCoercionRole, eqVarRole,
34 unwrapIP, wrapIP
35 ) where
36 #include "HsVersions.h"
37
38 import Var
39 import Coercion
40 import PprCore () -- Instance OutputableBndr TyVar
41 import TypeRep -- Knows type representation
42 import TcType
43 import Type
44 import TyCon
45 import Class( Class )
46 import CoAxiom
47 import PrelNames
48 import VarEnv
49 import VarSet
50 import Name
51
52 import Util
53 import Bag
54 import Pair
55 #if __GLASGOW_HASKELL__ < 709
56 import Control.Applicative
57 import Data.Traversable (traverse, sequenceA)
58 #endif
59 import qualified Data.Data as Data
60 import Outputable
61 import FastString
62 import SrcLoc
63 import Data.IORef( IORef )
64
65 {-
66 Note [TcCoercions]
67 ~~~~~~~~~~~~~~~~~~
68 | TcCoercions are a hack used by the typechecker. Normally,
69 Coercions have free variables of type (a ~# b): we call these
70 CoVars. However, the type checker passes around equality evidence
71 (boxed up) at type (a ~ b).
72
73 An TcCoercion is simply a Coercion whose free variables have the
74 boxed type (a ~ b). After we are done with typechecking the
75 desugarer finds the free variables, unboxes them, and creates a
76 resulting real Coercion with kosher free variables.
77
78 We can use most of the Coercion "smart constructors" to build TcCoercions.
79 However, mkCoVarCo will not work! The equivalent is mkTcCoVarCo.
80
81 The data type is similar to Coercion.Coercion, with the following
82 differences
83 * Most important, TcLetCo adds let-bindings for coercions.
84 This is what lets us unify two for-all types and generate
85 equality constraints underneath
86
87 * The kind of a TcCoercion is t1 ~ t2 (resp. Coercible t1 t2)
88 of a Coercion is t1 ~# t2 (resp. t1 ~#R t2)
89
90 * UnsafeCo aren't required, but we do have TcPhantomCo
91
92 * Representation invariants are weaker:
93 - we are allowed to have type synonyms in TcTyConAppCo
94 - the first arg of a TcAppCo can be a TcTyConAppCo
95 - TcSubCo is not applied as deep as done with mkSubCo
96 Reason: they'll get established when we desugar to Coercion
97
98 * TcAxiomInstCo has a [TcCoercion] parameter, and not a [Type] parameter.
99 This differs from the formalism, but corresponds to AxiomInstCo (see
100 [Coercion axioms applied to coercions]).
101
102 Note [mkTcTransAppCo]
103 ~~~~~~~~~~~~~~~~~~~~~
104 Suppose we have
105
106 co1 :: a ~R Maybe
107 co2 :: b ~R Int
108
109 and we want
110
111 co3 :: a b ~R Maybe Int
112
113 This seems sensible enough. But, we can't let (co3 = co1 co2), because
114 that's ill-roled! Note that mkTcAppCo requires a *nominal* second coercion.
115
116 The way around this is to use transitivity:
117
118 co3 = (co1 <b>_N) ; (Maybe co2) :: a b ~R Maybe Int
119
120 Or, it's possible everything is the other way around:
121
122 co1' :: Maybe ~R a
123 co2' :: Int ~R b
124
125 and we want
126
127 co3' :: Maybe Int ~R a b
128
129 then
130
131 co3' = (Maybe co2') ; (co1' <b>_N)
132
133 This is exactly what `mkTcTransAppCo` builds for us. Information for all
134 the arguments tends to be to hand at call sites, so it's quicker than
135 using, say, tcCoercionKind.
136 -}
137
138 type TcCoercionN = TcCoercion -- A Nominal corecion ~N
139 type TcCoercionR = TcCoercion -- A Representational corecion ~R
140
141 data TcCoercion
142 = TcRefl Role TcType
143 | TcTyConAppCo Role TyCon [TcCoercion]
144 | TcAppCo TcCoercion TcCoercion
145 | TcForAllCo TyVar TcCoercion
146 | TcCoVarCo EqVar
147 | TcAxiomInstCo (CoAxiom Branched) Int -- Int specifies branch number
148 [TcCoercion] -- See [CoAxiom Index] in Coercion.hs
149 -- This is number of types and coercions are expected to match to CoAxiomRule
150 -- (i.e., the CoAxiomRules are always fully saturated)
151 | TcAxiomRuleCo CoAxiomRule [TcType] [TcCoercion]
152 | TcPhantomCo TcType TcType
153 | TcSymCo TcCoercion
154 | TcTransCo TcCoercion TcCoercion
155 | TcNthCo Int TcCoercion
156 | TcLRCo LeftOrRight TcCoercion
157 | TcSubCo TcCoercion -- Argument is never TcRefl
158 | TcCastCo TcCoercion TcCoercion -- co1 |> co2
159 | TcLetCo TcEvBinds TcCoercion
160 | TcCoercion Coercion -- embed a Core Coercion
161 deriving (Data.Data, Data.Typeable)
162
163 isEqVar :: Var -> Bool
164 -- Is lifted coercion variable (only!)
165 isEqVar v = case tyConAppTyCon_maybe (varType v) of
166 Just tc -> tc `hasKey` eqTyConKey
167 Nothing -> False
168
169 isTcReflCo_maybe :: TcCoercion -> Maybe TcType
170 isTcReflCo_maybe (TcRefl _ ty) = Just ty
171 isTcReflCo_maybe (TcCoercion co) = isReflCo_maybe co
172 isTcReflCo_maybe _ = Nothing
173
174 isTcReflCo :: TcCoercion -> Bool
175 isTcReflCo (TcRefl {}) = True
176 isTcReflCo (TcCoercion co) = isReflCo co
177 isTcReflCo _ = False
178
179 getTcCoVar_maybe :: TcCoercion -> Maybe CoVar
180 getTcCoVar_maybe (TcCoVarCo v) = Just v
181 getTcCoVar_maybe _ = Nothing
182
183 mkTcReflCo :: Role -> TcType -> TcCoercion
184 mkTcReflCo = TcRefl
185
186 mkTcNomReflCo :: TcType -> TcCoercion
187 mkTcNomReflCo = TcRefl Nominal
188
189 mkTcRepReflCo :: TcType -> TcCoercion
190 mkTcRepReflCo = TcRefl Representational
191
192 mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
193 mkTcFunCo role co1 co2 = mkTcTyConAppCo role funTyCon [co1, co2]
194
195 mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion
196 mkTcTyConAppCo role tc cos -- No need to expand type synonyms
197 -- See Note [TcCoercions]
198 | Just tys <- traverse isTcReflCo_maybe cos
199 = TcRefl role (mkTyConApp tc tys) -- See Note [Refl invariant]
200
201 | otherwise = TcTyConAppCo role tc cos
202
203 -- Input coercion is Nominal
204 -- mkSubCo will do some normalisation. We do not do it for TcCoercions, but
205 -- defer that to desugaring; just to reduce the code duplication a little bit
206 mkTcSubCo :: TcCoercion -> TcCoercion
207 mkTcSubCo (TcRefl _ ty)
208 = TcRefl Representational ty
209 mkTcSubCo co
210 = ASSERT2( tcCoercionRole co == Nominal, ppr co)
211 TcSubCo co
212
213 -- See Note [Role twiddling functions] in Coercion
214 -- | Change the role of a 'TcCoercion'. Returns 'Nothing' if this isn't
215 -- a downgrade.
216 tcDowngradeRole_maybe :: Role -- desired role
217 -> Role -- current role
218 -> TcCoercion -> Maybe TcCoercion
219 tcDowngradeRole_maybe Representational Nominal = Just . mkTcSubCo
220 tcDowngradeRole_maybe Nominal Representational = const Nothing
221 tcDowngradeRole_maybe Phantom _
222 = panic "tcDowngradeRole_maybe Phantom"
223 -- not supported (not needed at the moment)
224 tcDowngradeRole_maybe _ Phantom = const Nothing
225 tcDowngradeRole_maybe _ _ = Just
226
227 -- See Note [Role twiddling functions] in Coercion
228 -- | Change the role of a 'TcCoercion'. Panics if this isn't a downgrade.
229 tcDowngradeRole :: Role -- ^ desired role
230 -> Role -- ^ current role
231 -> TcCoercion -> TcCoercion
232 tcDowngradeRole r1 r2 co
233 = case tcDowngradeRole_maybe r1 r2 co of
234 Just co' -> co'
235 Nothing -> pprPanic "tcDowngradeRole" (ppr r1 <+> ppr r2 <+> ppr co)
236
237 -- | If the EqRel is ReprEq, makes a TcSubCo; otherwise, does nothing.
238 -- Note that the input coercion should always be nominal.
239 maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
240 maybeTcSubCo NomEq = id
241 maybeTcSubCo ReprEq = mkTcSubCo
242
243 mkTcAxInstCo :: Role -> CoAxiom br -> Int -> [TcType] -> TcCoercion
244 mkTcAxInstCo role ax index tys
245 | ASSERT2( not (role == Nominal && ax_role == Representational) , ppr (ax, tys) )
246 arity == n_tys = tcDowngradeRole role ax_role $
247 TcAxiomInstCo ax_br index rtys
248 | otherwise = ASSERT( arity < n_tys )
249 tcDowngradeRole role ax_role $
250 foldl TcAppCo (TcAxiomInstCo ax_br index (take arity rtys))
251 (drop arity rtys)
252 where
253 n_tys = length tys
254 ax_br = toBranchedAxiom ax
255 branch = coAxiomNthBranch ax_br index
256 arity = length $ coAxBranchTyVars branch
257 ax_role = coAxiomRole ax
258 arg_roles = coAxBranchRoles branch
259 rtys = zipWith mkTcReflCo (arg_roles ++ repeat Nominal) tys
260
261 mkTcAxiomRuleCo :: CoAxiomRule -> [TcType] -> [TcCoercion] -> TcCoercion
262 mkTcAxiomRuleCo = TcAxiomRuleCo
263
264 mkTcUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [TcType] -> TcCoercion
265 mkTcUnbranchedAxInstCo role ax tys
266 = mkTcAxInstCo role ax 0 tys
267
268 mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion
269 -- No need to deal with TyConApp on the left; see Note [TcCoercions]
270 -- Second coercion *must* be nominal
271 mkTcAppCo (TcRefl r ty1) (TcRefl _ ty2) = TcRefl r (mkAppTy ty1 ty2)
272 mkTcAppCo co1 co2 = TcAppCo co1 co2
273
274 -- | Like `mkTcAppCo`, but allows the second coercion to be other than
275 -- nominal. See Note [mkTcTransAppCo]. Role r3 cannot be more stringent
276 -- than either r1 or r2.
277 mkTcTransAppCo :: Role -- ^ r1
278 -> TcCoercion -- ^ co1 :: ty1a ~r1 ty1b
279 -> TcType -- ^ ty1a
280 -> TcType -- ^ ty1b
281 -> Role -- ^ r2
282 -> TcCoercion -- ^ co2 :: ty2a ~r2 ty2b
283 -> TcType -- ^ ty2a
284 -> TcType -- ^ ty2b
285 -> Role -- ^ r3
286 -> TcCoercion -- ^ :: ty1a ty2a ~r3 ty1b ty2b
287 mkTcTransAppCo r1 co1 ty1a ty1b r2 co2 ty2a ty2b r3
288 -- How incredibly fiddly! Is there a better way??
289 = case (r1, r2, r3) of
290 (_, _, Phantom)
291 -> mkTcPhantomCo (mkAppTy ty1a ty2a) (mkAppTy ty1b ty2b)
292 (_, _, Nominal)
293 -> ASSERT( r1 == Nominal && r2 == Nominal )
294 mkTcAppCo co1 co2
295 (Nominal, Nominal, Representational)
296 -> mkTcSubCo (mkTcAppCo co1 co2)
297 (_, Nominal, Representational)
298 -> ASSERT( r1 == Representational )
299 mkTcAppCo co1 co2
300 (Nominal, Representational, Representational)
301 -> go (mkTcSubCo co1)
302 (_ , _, Representational)
303 -> ASSERT( r1 == Representational && r2 == Representational )
304 go co1
305 where
306 go co1_repr
307 | Just (tc1b, tys1b) <- tcSplitTyConApp_maybe ty1b
308 , nextRole ty1b == r2
309 = (co1_repr `mkTcAppCo` mkTcNomReflCo ty2a) `mkTcTransCo`
310 (mkTcTyConAppCo Representational tc1b
311 (zipWith mkTcReflCo (tyConRolesX Representational tc1b) tys1b
312 ++ [co2]))
313
314 | Just (tc1a, tys1a) <- tcSplitTyConApp_maybe ty1a
315 , nextRole ty1a == r2
316 = (mkTcTyConAppCo Representational tc1a
317 (zipWith mkTcReflCo (tyConRolesX Representational tc1a) tys1a
318 ++ [co2]))
319 `mkTcTransCo`
320 (co1_repr `mkTcAppCo` mkTcNomReflCo ty2b)
321
322 | otherwise
323 = pprPanic "mkTcTransAppCo" (vcat [ ppr r1, ppr co1, ppr ty1a, ppr ty1b
324 , ppr r2, ppr co2, ppr ty2a, ppr ty2b
325 , ppr r3 ])
326
327 mkTcSymCo :: TcCoercion -> TcCoercion
328 mkTcSymCo co@(TcRefl {}) = co
329 mkTcSymCo (TcSymCo co) = co
330 mkTcSymCo co = TcSymCo co
331
332 mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
333 mkTcTransCo (TcRefl {}) co = co
334 mkTcTransCo co (TcRefl {}) = co
335 mkTcTransCo co1 co2 = TcTransCo co1 co2
336
337 mkTcNthCo :: Int -> TcCoercion -> TcCoercion
338 mkTcNthCo n (TcRefl r ty) = TcRefl r (tyConAppArgN n ty)
339 mkTcNthCo n co = TcNthCo n co
340
341 mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
342 mkTcLRCo lr (TcRefl r ty) = TcRefl r (pickLR lr (tcSplitAppTy ty))
343 mkTcLRCo lr co = TcLRCo lr co
344
345 mkTcPhantomCo :: TcType -> TcType -> TcCoercion
346 mkTcPhantomCo = TcPhantomCo
347
348 mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion
349 mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys
350
351 mkTcForAllCo :: Var -> TcCoercion -> TcCoercion
352 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)
353 mkTcForAllCo tv (TcRefl r ty) = ASSERT( isTyVar tv ) TcRefl r (mkForAllTy tv ty)
354 mkTcForAllCo tv co = ASSERT( isTyVar tv ) TcForAllCo tv co
355
356 mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion
357 mkTcForAllCos tvs (TcRefl r ty) = ASSERT( all isTyVar tvs ) TcRefl r (mkForAllTys tvs ty)
358 mkTcForAllCos tvs co = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs
359
360 mkTcCoVarCo :: EqVar -> TcCoercion
361 -- ipv :: s ~ t (the boxed equality type) or Coercible s t (the boxed representational equality type)
362 mkTcCoVarCo ipv = TcCoVarCo ipv
363 -- Previously I checked for (ty ~ ty) and generated Refl,
364 -- but in fact ipv may not even (visibly) have a (t1 ~ t2) type, because
365 -- the constraint solver does not substitute in the types of
366 -- evidence variables as it goes. In any case, the optimisation
367 -- will be done in the later zonking phase
368
369 tcCoercionKind :: TcCoercion -> Pair Type
370 tcCoercionKind co = go co
371 where
372 go (TcRefl _ ty) = Pair ty ty
373 go (TcLetCo _ co) = go co
374 go (TcCastCo _ co) = case getEqPredTys (pSnd (go co)) of
375 (ty1,ty2) -> Pair ty1 ty2
376 go (TcTyConAppCo _ tc cos)= mkTyConApp tc <$> (sequenceA $ map go cos)
377 go (TcAppCo co1 co2) = mkAppTy <$> go co1 <*> go co2
378 go (TcForAllCo tv co) = mkForAllTy tv <$> go co
379 go (TcCoVarCo cv) = eqVarKind cv
380 go (TcAxiomInstCo ax ind cos)
381 = let branch = coAxiomNthBranch ax ind
382 tvs = coAxBranchTyVars branch
383 Pair tys1 tys2 = sequenceA (map go cos)
384 in ASSERT( cos `equalLength` tvs )
385 Pair (substTyWith tvs tys1 (coAxNthLHS ax ind))
386 (substTyWith tvs tys2 (coAxBranchRHS branch))
387 go (TcPhantomCo ty1 ty2) = Pair ty1 ty2
388 go (TcSymCo co) = swap (go co)
389 go (TcTransCo co1 co2) = Pair (pFst (go co1)) (pSnd (go co2))
390 go (TcNthCo d co) = tyConAppArgN d <$> go co
391 go (TcLRCo lr co) = (pickLR lr . tcSplitAppTy) <$> go co
392 go (TcSubCo co) = go co
393 go (TcAxiomRuleCo ax ts cs) =
394 case coaxrProves ax ts (map tcCoercionKind cs) of
395 Just res -> res
396 Nothing -> panic "tcCoercionKind: malformed TcAxiomRuleCo"
397 go (TcCoercion co) = coercionKind co
398
399 eqVarRole :: EqVar -> Role
400 eqVarRole cv = getEqPredRole (varType cv)
401
402 eqVarKind :: EqVar -> Pair Type
403 eqVarKind cv
404 | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)
405 = ASSERT(tc `hasKey` eqTyConKey)
406 Pair ty1 ty2
407 | otherwise = pprPanic "eqVarKind, non coercion variable" (ppr cv <+> dcolon <+> ppr (varType cv))
408
409 tcCoercionRole :: TcCoercion -> Role
410 tcCoercionRole = go
411 where
412 go (TcRefl r _) = r
413 go (TcTyConAppCo r _ _) = r
414 go (TcAppCo co _) = go co
415 go (TcForAllCo _ co) = go co
416 go (TcCoVarCo cv) = eqVarRole cv
417 go (TcAxiomInstCo ax _ _) = coAxiomRole ax
418 go (TcPhantomCo _ _) = Phantom
419 go (TcSymCo co) = go co
420 go (TcTransCo co1 _) = go co1 -- same as go co2
421 go (TcNthCo n co) = let Pair ty1 _ = tcCoercionKind co
422 (tc, _) = tcSplitTyConApp ty1
423 in nthRole (go co) tc n
424 go (TcLRCo _ _) = Nominal
425 go (TcSubCo _) = Representational
426 go (TcAxiomRuleCo c _ _) = coaxrRole c
427 go (TcCastCo c _) = go c
428 go (TcLetCo _ c) = go c
429 go (TcCoercion co) = coercionRole co
430
431
432 coVarsOfTcCo :: TcCoercion -> VarSet
433 -- Only works on *zonked* coercions, because of TcLetCo
434 coVarsOfTcCo tc_co
435 = go tc_co
436 where
437 go (TcRefl _ _) = emptyVarSet
438 go (TcTyConAppCo _ _ cos) = mapUnionVarSet go cos
439 go (TcAppCo co1 co2) = go co1 `unionVarSet` go co2
440 go (TcCastCo co1 co2) = go co1 `unionVarSet` go co2
441 go (TcForAllCo _ co) = go co
442 go (TcCoVarCo v) = unitVarSet v
443 go (TcAxiomInstCo _ _ cos) = mapUnionVarSet go cos
444 go (TcPhantomCo _ _) = emptyVarSet
445 go (TcSymCo co) = go co
446 go (TcTransCo co1 co2) = go co1 `unionVarSet` go co2
447 go (TcNthCo _ co) = go co
448 go (TcLRCo _ co) = go co
449 go (TcSubCo co) = go co
450 go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs
451 `minusVarSet` get_bndrs bs
452 go (TcLetCo {}) = emptyVarSet -- Harumph. This does legitimately happen in the call
453 -- to evVarsOfTerm in the DEBUG check of setEvBind
454 go (TcAxiomRuleCo _ _ cos) = mapUnionVarSet go cos
455 go (TcCoercion co) = -- the use of coVarsOfTcCo in dsTcCoercion will
456 -- fail if there are any proper, unlifted covars
457 ASSERT( isEmptyVarSet (coVarsOfCo co) )
458 emptyVarSet
459
460 -- We expect only coercion bindings, so use evTermCoercion
461 go_bind :: EvBind -> VarSet
462 go_bind (EvBind { eb_rhs =tm }) = go (evTermCoercion tm)
463
464 get_bndrs :: Bag EvBind -> VarSet
465 get_bndrs = foldrBag (\ (EvBind { eb_lhs = b }) bs -> extendVarSet bs b) emptyVarSet
466
467 -- Pretty printing
468
469 instance Outputable TcCoercion where
470 ppr = pprTcCo
471
472 pprTcCo, pprParendTcCo :: TcCoercion -> SDoc
473 pprTcCo co = ppr_co TopPrec co
474 pprParendTcCo co = ppr_co TyConPrec co
475
476 ppr_co :: TyPrec -> TcCoercion -> SDoc
477 ppr_co _ (TcRefl r ty) = angleBrackets (ppr ty) <> ppr_role r
478
479 ppr_co p co@(TcTyConAppCo _ tc [_,_])
480 | tc `hasKey` funTyConKey = ppr_fun_co p co
481
482 ppr_co p (TcTyConAppCo r tc cos) = pprTcApp p ppr_co tc cos <> ppr_role r
483 ppr_co p (TcLetCo bs co) = maybeParen p TopPrec $
484 sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]
485 ppr_co p (TcAppCo co1 co2) = maybeParen p TyConPrec $
486 pprTcCo co1 <+> ppr_co TyConPrec co2
487 ppr_co p (TcCastCo co1 co2) = maybeParen p FunPrec $
488 ppr_co FunPrec co1 <+> ptext (sLit "|>") <+> ppr_co FunPrec co2
489 ppr_co p co@(TcForAllCo {}) = ppr_forall_co p co
490
491 ppr_co _ (TcCoVarCo cv) = parenSymOcc (getOccName cv) (ppr cv)
492
493 ppr_co p (TcAxiomInstCo con ind cos)
494 = pprPrefixApp p (ppr (getName con) <> brackets (ppr ind)) (map pprParendTcCo cos)
495
496 ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $
497 ppr_co FunPrec co1
498 <+> ptext (sLit ";")
499 <+> ppr_co FunPrec co2
500 ppr_co p (TcPhantomCo t1 t2) = pprPrefixApp p (ptext (sLit "PhantomCo")) [pprParendType t1, pprParendType t2]
501 ppr_co p (TcSymCo co) = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]
502 ppr_co p (TcNthCo n co) = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]
503 ppr_co p (TcLRCo lr co) = pprPrefixApp p (ppr lr) [pprParendTcCo co]
504 ppr_co p (TcSubCo co) = pprPrefixApp p (ptext (sLit "Sub")) [pprParendTcCo co]
505 ppr_co p (TcAxiomRuleCo co ts ps) = maybeParen p TopPrec
506 $ ppr_tc_axiom_rule_co co ts ps
507 ppr_co p (TcCoercion co) = pprPrefixApp p (text "Core co:") [ppr co]
508
509 ppr_tc_axiom_rule_co :: CoAxiomRule -> [TcType] -> [TcCoercion] -> SDoc
510 ppr_tc_axiom_rule_co co ts ps = ppr (coaxrName co) <> ppTs ts $$ nest 2 (ppPs ps)
511 where
512 ppTs [] = Outputable.empty
513 ppTs [t] = ptext (sLit "@") <> ppr_type TopPrec t
514 ppTs ts = ptext (sLit "@") <>
515 parens (hsep $ punctuate comma $ map pprType ts)
516
517 ppPs [] = Outputable.empty
518 ppPs [p] = pprParendTcCo p
519 ppPs (p : ps) = ptext (sLit "(") <+> pprTcCo p $$
520 vcat [ ptext (sLit ",") <+> pprTcCo q | q <- ps ] $$
521 ptext (sLit ")")
522
523 ppr_role :: Role -> SDoc
524 ppr_role r = underscore <> pp_role
525 where pp_role = case r of
526 Nominal -> char 'N'
527 Representational -> char 'R'
528 Phantom -> char 'P'
529
530 ppr_fun_co :: TyPrec -> TcCoercion -> SDoc
531 ppr_fun_co p co = pprArrowChain p (split co)
532 where
533 split :: TcCoercion -> [SDoc]
534 split (TcTyConAppCo _ f [arg,res])
535 | f `hasKey` funTyConKey
536 = ppr_co FunPrec arg : split res
537 split co = [ppr_co TopPrec co]
538
539 ppr_forall_co :: TyPrec -> TcCoercion -> SDoc
540 ppr_forall_co p ty
541 = maybeParen p FunPrec $
542 sep [pprForAll tvs, ppr_co TopPrec rho]
543 where
544 (tvs, rho) = split1 [] ty
545 split1 tvs (TcForAllCo tv ty) = split1 (tv:tvs) ty
546 split1 tvs ty = (reverse tvs, ty)
547
548 {-
549 ************************************************************************
550 * *
551 HsWrapper
552 * *
553 ************************************************************************
554 -}
555
556 data HsWrapper
557 = WpHole -- The identity coercion
558
559 | WpCompose HsWrapper HsWrapper
560 -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
561 --
562 -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. [])
563 -- But ([] a) `WpCompose` ([] b) = ([] b a)
564
565 | WpFun HsWrapper HsWrapper TcType TcType
566 -- (WpFun wrap1 wrap2 t1 t2)[e] = \(x:t1). wrap2[ e wrap1[x] ] :: t2
567 -- So note that if wrap1 :: exp_arg <= act_arg
568 -- wrap2 :: act_res <= exp_res
569 -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res)
570 -- This isn't the same as for mkTcFunCo, but it has to be this way
571 -- because we can't use 'sym' to flip around these HsWrappers
572
573 | WpCast TcCoercion -- A cast: [] `cast` co
574 -- Guaranteed not the identity coercion
575 -- At role Representational
576
577 -- Evidence abstraction and application
578 -- (both dictionaries and coercions)
579 | WpEvLam EvVar -- \d. [] the 'd' is an evidence variable
580 | WpEvApp EvTerm -- [] d the 'd' is evidence for a constraint
581
582 -- Kind and Type abstraction and application
583 | WpTyLam TyVar -- \a. [] the 'a' is a type/kind variable (not coercion var)
584 | WpTyApp KindOrType -- [] t the 't' is a type (not coercion)
585
586
587 | WpLet TcEvBinds -- Non-empty (or possibly non-empty) evidence bindings,
588 -- so that the identity coercion is always exactly WpHole
589 deriving (Data.Data, Data.Typeable)
590
591
592 (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
593 WpHole <.> c = c
594 c <.> WpHole = c
595 c1 <.> c2 = c1 `WpCompose` c2
596
597 mkWpFun :: HsWrapper -> HsWrapper -> TcType -> TcType -> HsWrapper
598 mkWpFun WpHole WpHole _ _ = WpHole
599 mkWpFun WpHole (WpCast co2) t1 _ = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2)
600 mkWpFun (WpCast co1) WpHole _ t2 = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2))
601 mkWpFun (WpCast co1) (WpCast co2) _ _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2)
602 mkWpFun co1 co2 t1 t2 = WpFun co1 co2 t1 t2
603
604 mkWpCast :: TcCoercion -> HsWrapper
605 mkWpCast co
606 | isTcReflCo co = WpHole
607 | otherwise = ASSERT2(tcCoercionRole co == Representational, ppr co)
608 WpCast co
609
610 mkWpTyApps :: [Type] -> HsWrapper
611 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
612
613 mkWpEvApps :: [EvTerm] -> HsWrapper
614 mkWpEvApps args = mk_co_app_fn WpEvApp args
615
616 mkWpEvVarApps :: [EvVar] -> HsWrapper
617 mkWpEvVarApps vs = mkWpEvApps (map EvId vs)
618
619 mkWpTyLams :: [TyVar] -> HsWrapper
620 mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
621
622 mkWpLams :: [Var] -> HsWrapper
623 mkWpLams ids = mk_co_lam_fn WpEvLam ids
624
625 mkWpLet :: TcEvBinds -> HsWrapper
626 -- This no-op is a quite a common case
627 mkWpLet (EvBinds b) | isEmptyBag b = WpHole
628 mkWpLet ev_binds = WpLet ev_binds
629
630 mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
631 mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as
632
633 mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
634 -- For applications, the *first* argument must
635 -- come *last* in the composition sequence
636 mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as
637
638 idHsWrapper :: HsWrapper
639 idHsWrapper = WpHole
640
641 isIdHsWrapper :: HsWrapper -> Bool
642 isIdHsWrapper WpHole = True
643 isIdHsWrapper _ = False
644
645 {-
646 ************************************************************************
647 * *
648 Evidence bindings
649 * *
650 ************************************************************************
651 -}
652
653 data TcEvBinds
654 = TcEvBinds -- Mutable evidence bindings
655 EvBindsVar -- Mutable because they are updated "later"
656 -- when an implication constraint is solved
657
658 | EvBinds -- Immutable after zonking
659 (Bag EvBind)
660
661 deriving( Data.Typeable )
662
663 data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique
664 -- The Unique is only for debug printing
665
666 instance Data.Data TcEvBinds where
667 -- Placeholder; we can't travers into TcEvBinds
668 toConstr _ = abstractConstr "TcEvBinds"
669 gunfold _ _ = error "gunfold"
670 dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
671
672 -----------------
673 newtype EvBindMap
674 = EvBindMap {
675 ev_bind_varenv :: VarEnv EvBind
676 } -- Map from evidence variables to evidence terms
677
678 emptyEvBindMap :: EvBindMap
679 emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv }
680
681 extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
682 extendEvBinds bs ev_bind
683 = EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs)
684 (eb_lhs ev_bind)
685 ev_bind }
686
687 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
688 lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs)
689
690 evBindMapBinds :: EvBindMap -> Bag EvBind
691 evBindMapBinds = foldEvBindMap consBag emptyBag
692
693 foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
694 foldEvBindMap k z bs = foldVarEnv k z (ev_bind_varenv bs)
695
696 -----------------
697 -- All evidence is bound by EvBinds; no side effects
698 data EvBind
699 = EvBind { eb_lhs :: EvVar
700 , eb_rhs :: EvTerm
701 , eb_is_given :: Bool -- True <=> given
702 -- See Note [Tracking redundant constraints] in TcSimplify
703 }
704
705 mkWantedEvBind :: EvVar -> EvTerm -> EvBind
706 mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm }
707
708 mkGivenEvBind :: EvVar -> EvTerm -> EvBind
709 mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm }
710
711 data EvTerm
712 = EvId EvId -- Any sort of evidence Id, including coercions
713
714 | EvCoercion TcCoercion -- (Boxed) coercion bindings
715 -- See Note [Coercion evidence terms]
716
717 | EvCast EvTerm TcCoercion -- d |> co, the coercion being at role representational
718
719 | EvDFunApp DFunId -- Dictionary instance application
720 [Type] [EvId]
721
722 | EvDelayedError Type FastString -- Used with Opt_DeferTypeErrors
723 -- See Note [Deferring coercion errors to runtime]
724 -- in TcSimplify
725
726 | EvSuperClass EvTerm Int -- n'th superclass. Used for both equalities and
727 -- dictionaries, even though the former have no
728 -- selector Id. We count up from _0_
729
730 | EvLit EvLit -- Dictionary for KnownNat and KnownSymbol classes.
731 -- Note [KnownNat & KnownSymbol and EvLit]
732
733 | EvCallStack EvCallStack -- Dictionary for CallStack implicit parameters
734
735 | EvTypeable Type EvTypeable -- Dictionary for (Typeable ty)
736
737 deriving( Data.Data, Data.Typeable )
738
739
740 -- | Instructions on how to make a 'Typeable' dictionary.
741 -- See Note [Typeable evidence terms]
742 data EvTypeable
743 = EvTypeableTyCon -- ^ Dictionary for @Typeable (T k1..kn)@
744
745 | EvTypeableTyApp EvTerm EvTerm
746 -- ^ Dictionary for @Typeable (s t)@,
747 -- given a dictionaries for @s@ and @t@
748
749 | EvTypeableTyLit EvTerm
750 -- ^ Dictionary for a type literal,
751 -- e.g. @Typeable "foo"@ or @Typeable 3@
752 -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@
753 -- (see Trac #10348)
754
755 deriving ( Data.Data, Data.Typeable )
756
757 data EvLit
758 = EvNum Integer
759 | EvStr FastString
760 deriving( Data.Data, Data.Typeable )
761
762 -- | Evidence for @CallStack@ implicit parameters.
763 data EvCallStack
764 -- See Note [Overview of implicit CallStacks]
765 = EvCsEmpty
766 | EvCsPushCall Name RealSrcSpan EvTerm
767 -- ^ @EvCsPushCall name loc stk@ represents a call to @name@, occurring at
768 -- @loc@, in a calling context @stk@.
769 | EvCsTop FastString RealSrcSpan EvTerm
770 -- ^ @EvCsTop name loc stk@ represents a use of an implicit parameter
771 -- @?name@, occurring at @loc@, in a calling context @stk@.
772 deriving( Data.Data, Data.Typeable )
773
774 {-
775 Note [Typeable evidence terms]
776 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
777 The EvTypeable data type looks isomorphic to Type, but the EvTerms
778 inside can be EvIds. Eg
779 f :: forall a. Typeable a => a -> TypeRep
780 f x = typeRep (undefined :: Proxy [a])
781 Here for the (Typeable [a]) dictionary passed to typeRep we make
782 evidence
783 dl :: Typeable [a] = EvTypeable [a]
784 (EvTypeableTyApp EvTypeableTyCon (EvId d))
785 where
786 d :: Typable a
787 is the lambda-bound dictionary passed into f.
788
789 Note [Coercion evidence terms]
790 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
791 A "coercion evidence term" takes one of these forms
792 co_tm ::= EvId v where v :: t1 ~ t2
793 | EvCoercion co
794 | EvCast co_tm co
795
796 We do quite often need to get a TcCoercion from an EvTerm; see
797 'evTermCoercion'.
798
799 INVARIANT: The evidence for any constraint with type (t1~t2) is
800 a coercion evidence term. Consider for example
801 [G] d :: F Int a
802 If we have
803 ax7 a :: F Int a ~ (a ~ Bool)
804 then we do NOT generate the constraint
805 [G] (d |> ax7 a) :: a ~ Bool
806 because that does not satisfy the invariant (d is not a coercion variable).
807 Instead we make a binding
808 g1 :: a~Bool = g |> ax7 a
809 and the constraint
810 [G] g1 :: a~Bool
811 See Trac [7238] and Note [Bind new Givens immediately] in TcRnTypes
812
813 Note [EvBinds/EvTerm]
814 ~~~~~~~~~~~~~~~~~~~~~
815 How evidence is created and updated. Bindings for dictionaries,
816 and coercions and implicit parameters are carried around in TcEvBinds
817 which during constraint generation and simplification is always of the
818 form (TcEvBinds ref). After constraint simplification is finished it
819 will be transformed to t an (EvBinds ev_bag).
820
821 Evidence for coercions *SHOULD* be filled in using the TcEvBinds
822 However, all EvVars that correspond to *wanted* coercion terms in
823 an EvBind must be mutable variables so that they can be readily
824 inlined (by zonking) after constraint simplification is finished.
825
826 Conclusion: a new wanted coercion variable should be made mutable.
827 [Notice though that evidence variables that bind coercion terms
828 from super classes will be "given" and hence rigid]
829
830
831 Note [KnownNat & KnownSymbol and EvLit]
832 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
833 A part of the type-level literals implementation are the classes
834 "KnownNat" and "KnownSymbol", which provide a "smart" constructor for
835 defining singleton values. Here is the key stuff from GHC.TypeLits
836
837 class KnownNat (n :: Nat) where
838 natSing :: SNat n
839
840 newtype SNat (n :: Nat) = SNat Integer
841
842 Conceptually, this class has infinitely many instances:
843
844 instance KnownNat 0 where natSing = SNat 0
845 instance KnownNat 1 where natSing = SNat 1
846 instance KnownNat 2 where natSing = SNat 2
847 ...
848
849 In practice, we solve `KnownNat` predicates in the type-checker
850 (see typecheck/TcInteract.hs) because we can't have infinately many instances.
851 The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
852
853 We make the following assumptions about dictionaries in GHC:
854 1. The "dictionary" for classes with a single method---like `KnownNat`---is
855 a newtype for the type of the method, so using a evidence amounts
856 to a coercion, and
857 2. Newtypes use the same representation as their definition types.
858
859 So, the evidence for `KnownNat` is just a value of the representation type,
860 wrapped in two newtype constructors: one to make it into a `SNat` value,
861 and another to make it into a `KnownNat` dictionary.
862
863 Also note that `natSing` and `SNat` are never actually exposed from the
864 library---they are just an implementation detail. Instead, users see
865 a more convenient function, defined in terms of `natSing`:
866
867 natVal :: KnownNat n => proxy n -> Integer
868
869 The reason we don't use this directly in the class is that it is simpler
870 and more efficient to pass around an integer rather than an entier function,
871 especialy when the `KnowNat` evidence is packaged up in an existential.
872
873 The story for kind `Symbol` is analogous:
874 * class KnownSymbol
875 * newtype SSymbol
876 * Evidence: EvLit (EvStr n)
877
878
879 Note [Overview of implicit CallStacks]
880 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
881 (See https://ghc.haskell.org/trac/ghc/wiki/ExplicitCallStack/ImplicitLocations)
882
883 The goal of CallStack evidence terms is to reify locations
884 in the program source as runtime values, without any support
885 from the RTS. We accomplish this by assigning a special meaning
886 to implicit parameters of type GHC.Stack.CallStack. A use of
887 a CallStack IP, e.g.
888
889 head [] = error (show (?loc :: CallStack))
890 head (x:_) = x
891
892 will be solved with the source location that gave rise to the IP
893 constraint (here, the use of ?loc). If there is already
894 a CallStack IP in scope, e.g. passed-in as an argument
895
896 head :: (?loc :: CallStack) => [a] -> a
897 head [] = error (show (?loc :: CallStack))
898 head (x:_) = x
899
900 we will push the new location onto the CallStack that was passed
901 in. These two cases are reflected by the EvCallStack evidence
902 type. In the first case, we will create an evidence term
903
904 EvCsTop "?loc" <?loc's location> EvCsEmpty
905
906 and in the second we'll have a given constraint
907
908 [G] d :: IP "loc" CallStack
909
910 in scope, and will create an evidence term
911
912 EvCsTop "?loc" <?loc's location> d
913
914 When we call a function that uses a CallStack IP, e.g.
915
916 f = head xs
917
918 we create an evidence term
919
920 EvCsPushCall "head" <head's location> EvCsEmpty
921
922 again pushing onto a given evidence term if one exists.
923
924 This provides a lightweight mechanism for building up call-stacks
925 explicitly, but is notably limited by the fact that the stack will
926 stop at the first function whose type does not include a CallStack IP.
927 For example, using the above definition of head:
928
929 f :: [a] -> a
930 f = head
931
932 g = f []
933
934 the resulting CallStack will include use of ?loc inside head and
935 the call to head inside f, but NOT the call to f inside g, because f
936 did not explicitly request a CallStack.
937
938 Important Details:
939 - GHC should NEVER report an insoluble CallStack constraint.
940
941 - A CallStack (defined in GHC.Stack) is a [(String, SrcLoc)], where the String
942 is the name of the binder that is used at the SrcLoc. SrcLoc is defined in
943 GHC.SrcLoc and contains the package/module/file name, as well as the full
944 source-span. Both CallStack and SrcLoc are kept abstract so only GHC can
945 construct new values.
946
947 - Consider the use of ?stk in:
948
949 head :: (?stk :: CallStack) => [a] -> a
950 head [] = error (show ?stk)
951
952 When solving the use of ?stk we'll have a given
953
954 [G] d :: IP "stk" CallStack
955
956 in scope. In the interaction phase, GHC would normally solve the use of ?stk
957 directly from the given, i.e. re-using the dicionary. But this is NOT what we
958 want! We want to generate a *new* CallStack with ?loc's SrcLoc pushed onto
959 the given CallStack. So we must take care in TcInteract.interactDict to
960 prioritize solving wanted CallStacks.
961
962 - We will automatically solve any wanted CallStack regardless of the name of the
963 IP, i.e.
964
965 f = show (?stk :: CallStack)
966 g = show (?loc :: CallStack)
967
968 are both valid. However, we will only push new SrcLocs onto existing
969 CallStacks when the IP names match, e.g. in
970
971 head :: (?loc :: CallStack) => [a] -> a
972 head [] = error (show (?stk :: CallStack))
973
974 the printed CallStack will NOT include head's call-site. This reflects the
975 standard scoping rules of implicit-parameters. (See TcInteract.interactDict)
976
977 - An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
978 The desugarer will need to unwrap the IP newtype before pushing a new
979 call-site onto a given stack (See DsBinds.dsEvCallStack)
980
981 - We only want to intercept constraints that arose due to the use of an IP or a
982 function call. In particular, we do NOT want to intercept the
983
984 (?stk :: CallStack) => [a] -> a
985 ~
986 (?stk :: CallStack) => [a] -> a
987
988 constraint that arises from the ambiguity check on `head`s type signature.
989 (See TcEvidence.isCallStackIP)
990 -}
991
992 mkEvCast :: EvTerm -> TcCoercion -> EvTerm
993 mkEvCast ev lco
994 | ASSERT2(tcCoercionRole lco == Representational, (vcat [ptext (sLit "Coercion of wrong role passed to mkEvCast:"), ppr ev, ppr lco]))
995 isTcReflCo lco = ev
996 | otherwise = EvCast ev lco
997
998 mkEvScSelectors :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
999 mkEvScSelectors ev cls tys
1000 = zipWith mk_pr (immSuperClasses cls tys) [0..]
1001 where
1002 mk_pr pred i = (pred, EvSuperClass ev i)
1003
1004 emptyTcEvBinds :: TcEvBinds
1005 emptyTcEvBinds = EvBinds emptyBag
1006
1007 isEmptyTcEvBinds :: TcEvBinds -> Bool
1008 isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
1009 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
1010
1011
1012 evTermCoercion :: EvTerm -> TcCoercion
1013 -- Applied only to EvTerms of type (s~t)
1014 -- See Note [Coercion evidence terms]
1015 evTermCoercion (EvId v) = mkTcCoVarCo v
1016 evTermCoercion (EvCoercion co) = co
1017 evTermCoercion (EvCast tm co) = TcCastCo (evTermCoercion tm) co
1018 evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
1019
1020 evVarsOfTerm :: EvTerm -> VarSet
1021 evVarsOfTerm (EvId v) = unitVarSet v
1022 evVarsOfTerm (EvCoercion co) = coVarsOfTcCo co
1023 evVarsOfTerm (EvDFunApp _ _ evs) = mkVarSet evs
1024 evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v
1025 evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
1026 evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
1027 evVarsOfTerm (EvLit _) = emptyVarSet
1028 evVarsOfTerm (EvCallStack cs) = evVarsOfCallStack cs
1029 evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev
1030
1031 evVarsOfTerms :: [EvTerm] -> VarSet
1032 evVarsOfTerms = mapUnionVarSet evVarsOfTerm
1033
1034 evVarsOfCallStack :: EvCallStack -> VarSet
1035 evVarsOfCallStack cs = case cs of
1036 EvCsEmpty -> emptyVarSet
1037 EvCsTop _ _ tm -> evVarsOfTerm tm
1038 EvCsPushCall _ _ tm -> evVarsOfTerm tm
1039
1040 evVarsOfTypeable :: EvTypeable -> VarSet
1041 evVarsOfTypeable ev =
1042 case ev of
1043 EvTypeableTyCon -> emptyVarSet
1044 EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
1045 EvTypeableTyLit e -> evVarsOfTerm e
1046
1047 {-
1048 ************************************************************************
1049 * *
1050 Pretty printing
1051 * *
1052 ************************************************************************
1053 -}
1054
1055 instance Outputable HsWrapper where
1056 ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn
1057
1058 pprHsWrapper :: SDoc -> HsWrapper -> SDoc
1059 -- In debug mode, print the wrapper
1060 -- otherwise just print what's inside
1061 pprHsWrapper doc wrap
1062 = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)
1063 where
1064 help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
1065 -- True <=> appears in function application position
1066 -- False <=> appears as body of let or lambda
1067 help it WpHole = it
1068 help it (WpCompose f1 f2) = help (help it f2) f1
1069 help it (WpFun f1 f2 t1 _) = add_parens $ ptext (sLit "\\(x") <> dcolon <> ppr t1 <> ptext (sLit ").") <+>
1070 help (\_ -> it True <+> help (\_ -> ptext (sLit "x")) f1 True) f2 False
1071 help it (WpCast co) = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")
1072 <+> pprParendTcCo co)]
1073 help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)]
1074 help it (WpTyApp ty) = no_parens $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
1075 help it (WpEvLam id) = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
1076 help it (WpTyLam tv) = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]
1077 help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
1078
1079 pp_bndr v = pprBndr LambdaBind v <> dot
1080
1081 add_parens, no_parens :: SDoc -> Bool -> SDoc
1082 add_parens d True = parens d
1083 add_parens d False = d
1084 no_parens d _ = d
1085
1086 instance Outputable TcEvBinds where
1087 ppr (TcEvBinds v) = ppr v
1088 ppr (EvBinds bs) = ptext (sLit "EvBinds") <> braces (vcat (map ppr (bagToList bs)))
1089
1090 instance Outputable EvBindsVar where
1091 ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)
1092
1093 instance Outputable EvBind where
1094 ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
1095 = sep [ pp_gw <+> ppr v
1096 , nest 2 $ equals <+> ppr e ]
1097 where
1098 pp_gw = brackets (if is_given then char 'G' else char 'W')
1099 -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
1100
1101 instance Outputable EvTerm where
1102 ppr (EvId v) = ppr v
1103 ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
1104 ppr (EvCoercion co) = ptext (sLit "CO") <+> ppr co
1105 ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
1106 ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
1107 ppr (EvLit l) = ppr l
1108 ppr (EvCallStack cs) = ppr cs
1109 ppr (EvDelayedError ty msg) = ptext (sLit "error")
1110 <+> sep [ char '@' <> ppr ty, ppr msg ]
1111 ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> ptext (sLit "Typeable") <+> ppr ty
1112
1113 instance Outputable EvLit where
1114 ppr (EvNum n) = integer n
1115 ppr (EvStr s) = text (show s)
1116
1117 instance Outputable EvCallStack where
1118 ppr EvCsEmpty
1119 = ptext (sLit "[]")
1120 ppr (EvCsTop name loc tm)
1121 = angleBrackets (ppr (name,loc)) <+> ptext (sLit ":") <+> ppr tm
1122 ppr (EvCsPushCall name loc tm)
1123 = angleBrackets (ppr (name,loc)) <+> ptext (sLit ":") <+> ppr tm
1124
1125 instance Outputable EvTypeable where
1126 ppr EvTypeableTyCon = ptext (sLit "TC")
1127 ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2)
1128 ppr (EvTypeableTyLit t1) = ptext (sLit "TyLit") <> ppr t1
1129
1130
1131 ----------------------------------------------------------------------
1132 -- Helper functions for dealing with IP newtype-dictionaries
1133 ----------------------------------------------------------------------
1134
1135 -- | Create a 'Coercion' that unwraps an implicit-parameter dictionary
1136 -- to expose the underlying value. We expect the 'Type' to have the form
1137 -- `IP sym ty`, return a 'Coercion' `co :: IP sym ty ~ ty`.
1138 unwrapIP :: Type -> Coercion
1139 unwrapIP ty =
1140 case unwrapNewTyCon_maybe tc of
1141 Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys
1142 Nothing -> pprPanic "unwrapIP" $
1143 text "The dictionary for" <+> quotes (ppr tc)
1144 <+> text "is not a newtype!"
1145 where
1146 (tc, tys) = splitTyConApp ty
1147
1148 -- | Create a 'Coercion' that wraps a value in an implicit-parameter
1149 -- dictionary. See 'unwrapIP'.
1150 wrapIP :: Type -> Coercion
1151 wrapIP ty = mkSymCo (unwrapIP ty)