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