83bbcca1b738ac856bb0c6f4416973493879f755
[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 EvTypeable -- Dictionary for `Typeable`
736
737 deriving( Data.Data, Data.Typeable )
738
739
740 -- | Instructions on how to make a 'Typeable' dictionary.
741 data EvTypeable
742 = EvTypeableTyCon TyCon [Kind]
743 -- ^ Dictionary for concrete type constructors.
744
745 | EvTypeableTyApp (EvTerm,Type) (EvTerm,Type)
746 -- ^ Dictionary for type applications; this is used when we have
747 -- a type expression starting with a type variable (e.g., @Typeable (f a)@)
748
749 | EvTypeableTyLit (EvTerm,Type)
750 -- ^ Dictionary for a type literal.
751
752 deriving ( Data.Data, Data.Typeable )
753
754 data EvLit
755 = EvNum Integer
756 | EvStr FastString
757 deriving( Data.Data, Data.Typeable )
758
759 -- | Evidence for @CallStack@ implicit parameters.
760 data EvCallStack
761 -- See Note [Overview of implicit CallStacks]
762 = EvCsEmpty
763 | EvCsPushCall Name RealSrcSpan EvTerm
764 -- ^ @EvCsPushCall name loc stk@ represents a call to @name@, occurring at
765 -- @loc@, in a calling context @stk@.
766 | EvCsTop FastString RealSrcSpan EvTerm
767 -- ^ @EvCsTop name loc stk@ represents a use of an implicit parameter
768 -- @?name@, occurring at @loc@, in a calling context @stk@.
769 deriving( Data.Data, Data.Typeable )
770
771 {-
772 Note [Coercion evidence terms]
773 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
774 A "coercion evidence term" takes one of these forms
775 co_tm ::= EvId v where v :: t1 ~ t2
776 | EvCoercion co
777 | EvCast co_tm co
778
779 We do quite often need to get a TcCoercion from an EvTerm; see
780 'evTermCoercion'.
781
782 INVARIANT: The evidence for any constraint with type (t1~t2) is
783 a coercion evidence term. Consider for example
784 [G] d :: F Int a
785 If we have
786 ax7 a :: F Int a ~ (a ~ Bool)
787 then we do NOT generate the constraint
788 [G] (d |> ax7 a) :: a ~ Bool
789 because that does not satisfy the invariant (d is not a coercion variable).
790 Instead we make a binding
791 g1 :: a~Bool = g |> ax7 a
792 and the constraint
793 [G] g1 :: a~Bool
794 See Trac [7238] and Note [Bind new Givens immediately] in TcRnTypes
795
796 Note [EvBinds/EvTerm]
797 ~~~~~~~~~~~~~~~~~~~~~
798 How evidence is created and updated. Bindings for dictionaries,
799 and coercions and implicit parameters are carried around in TcEvBinds
800 which during constraint generation and simplification is always of the
801 form (TcEvBinds ref). After constraint simplification is finished it
802 will be transformed to t an (EvBinds ev_bag).
803
804 Evidence for coercions *SHOULD* be filled in using the TcEvBinds
805 However, all EvVars that correspond to *wanted* coercion terms in
806 an EvBind must be mutable variables so that they can be readily
807 inlined (by zonking) after constraint simplification is finished.
808
809 Conclusion: a new wanted coercion variable should be made mutable.
810 [Notice though that evidence variables that bind coercion terms
811 from super classes will be "given" and hence rigid]
812
813
814 Note [KnownNat & KnownSymbol and EvLit]
815 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
816 A part of the type-level literals implementation are the classes
817 "KnownNat" and "KnownSymbol", which provide a "smart" constructor for
818 defining singleton values. Here is the key stuff from GHC.TypeLits
819
820 class KnownNat (n :: Nat) where
821 natSing :: SNat n
822
823 newtype SNat (n :: Nat) = SNat Integer
824
825 Conceptually, this class has infinitely many instances:
826
827 instance KnownNat 0 where natSing = SNat 0
828 instance KnownNat 1 where natSing = SNat 1
829 instance KnownNat 2 where natSing = SNat 2
830 ...
831
832 In practice, we solve `KnownNat` predicates in the type-checker
833 (see typecheck/TcInteract.hs) because we can't have infinately many instances.
834 The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
835
836 We make the following assumptions about dictionaries in GHC:
837 1. The "dictionary" for classes with a single method---like `KnownNat`---is
838 a newtype for the type of the method, so using a evidence amounts
839 to a coercion, and
840 2. Newtypes use the same representation as their definition types.
841
842 So, the evidence for `KnownNat` is just a value of the representation type,
843 wrapped in two newtype constructors: one to make it into a `SNat` value,
844 and another to make it into a `KnownNat` dictionary.
845
846 Also note that `natSing` and `SNat` are never actually exposed from the
847 library---they are just an implementation detail. Instead, users see
848 a more convenient function, defined in terms of `natSing`:
849
850 natVal :: KnownNat n => proxy n -> Integer
851
852 The reason we don't use this directly in the class is that it is simpler
853 and more efficient to pass around an integer rather than an entier function,
854 especialy when the `KnowNat` evidence is packaged up in an existential.
855
856 The story for kind `Symbol` is analogous:
857 * class KnownSymbol
858 * newtype SSymbol
859 * Evidence: EvLit (EvStr n)
860
861
862 Note [Overview of implicit CallStacks]
863 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
864 (See https://ghc.haskell.org/trac/ghc/wiki/ExplicitCallStack/ImplicitLocations)
865
866 The goal of CallStack evidence terms is to reify locations
867 in the program source as runtime values, without any support
868 from the RTS. We accomplish this by assigning a special meaning
869 to implicit parameters of type GHC.Stack.CallStack. A use of
870 a CallStack IP, e.g.
871
872 head [] = error (show (?loc :: CallStack))
873 head (x:_) = x
874
875 will be solved with the source location that gave rise to the IP
876 constraint (here, the use of ?loc). If there is already
877 a CallStack IP in scope, e.g. passed-in as an argument
878
879 head :: (?loc :: CallStack) => [a] -> a
880 head [] = error (show (?loc :: CallStack))
881 head (x:_) = x
882
883 we will push the new location onto the CallStack that was passed
884 in. These two cases are reflected by the EvCallStack evidence
885 type. In the first case, we will create an evidence term
886
887 EvCsTop "?loc" <?loc's location> EvCsEmpty
888
889 and in the second we'll have a given constraint
890
891 [G] d :: IP "loc" CallStack
892
893 in scope, and will create an evidence term
894
895 EvCsTop "?loc" <?loc's location> d
896
897 When we call a function that uses a CallStack IP, e.g.
898
899 f = head xs
900
901 we create an evidence term
902
903 EvCsPushCall "head" <head's location> EvCsEmpty
904
905 again pushing onto a given evidence term if one exists.
906
907 This provides a lightweight mechanism for building up call-stacks
908 explicitly, but is notably limited by the fact that the stack will
909 stop at the first function whose type does not include a CallStack IP.
910 For example, using the above definition of head:
911
912 f :: [a] -> a
913 f = head
914
915 g = f []
916
917 the resulting CallStack will include use of ?loc inside head and
918 the call to head inside f, but NOT the call to f inside g, because f
919 did not explicitly request a CallStack.
920
921 Important Details:
922 - GHC should NEVER report an insoluble CallStack constraint.
923
924 - A CallStack (defined in GHC.Stack) is a [(String, SrcLoc)], where the String
925 is the name of the binder that is used at the SrcLoc. SrcLoc is defined in
926 GHC.SrcLoc and contains the package/module/file name, as well as the full
927 source-span. Both CallStack and SrcLoc are kept abstract so only GHC can
928 construct new values.
929
930 - Consider the use of ?stk in:
931
932 head :: (?stk :: CallStack) => [a] -> a
933 head [] = error (show ?stk)
934
935 When solving the use of ?stk we'll have a given
936
937 [G] d :: IP "stk" CallStack
938
939 in scope. In the interaction phase, GHC would normally solve the use of ?stk
940 directly from the given, i.e. re-using the dicionary. But this is NOT what we
941 want! We want to generate a *new* CallStack with ?loc's SrcLoc pushed onto
942 the given CallStack. So we must take care in TcInteract.interactDict to
943 prioritize solving wanted CallStacks.
944
945 - We will automatically solve any wanted CallStack regardless of the name of the
946 IP, i.e.
947
948 f = show (?stk :: CallStack)
949 g = show (?loc :: CallStack)
950
951 are both valid. However, we will only push new SrcLocs onto existing
952 CallStacks when the IP names match, e.g. in
953
954 head :: (?loc :: CallStack) => [a] -> a
955 head [] = error (show (?stk :: CallStack))
956
957 the printed CallStack will NOT include head's call-site. This reflects the
958 standard scoping rules of implicit-parameters. (See TcInteract.interactDict)
959
960 - An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
961 The desugarer will need to unwrap the IP newtype before pushing a new
962 call-site onto a given stack (See DsBinds.dsEvCallStack)
963
964 - We only want to intercept constraints that arose due to the use of an IP or a
965 function call. In particular, we do NOT want to intercept the
966
967 (?stk :: CallStack) => [a] -> a
968 ~
969 (?stk :: CallStack) => [a] -> a
970
971 constraint that arises from the ambiguity check on `head`s type signature.
972 (See TcEvidence.isCallStackIP)
973 -}
974
975 mkEvCast :: EvTerm -> TcCoercion -> EvTerm
976 mkEvCast ev lco
977 | ASSERT2(tcCoercionRole lco == Representational, (vcat [ptext (sLit "Coercion of wrong role passed to mkEvCast:"), ppr ev, ppr lco]))
978 isTcReflCo lco = ev
979 | otherwise = EvCast ev lco
980
981 mkEvScSelectors :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
982 mkEvScSelectors ev cls tys
983 = zipWith mk_pr (immSuperClasses cls tys) [0..]
984 where
985 mk_pr pred i = (pred, EvSuperClass ev i)
986
987 emptyTcEvBinds :: TcEvBinds
988 emptyTcEvBinds = EvBinds emptyBag
989
990 isEmptyTcEvBinds :: TcEvBinds -> Bool
991 isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
992 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
993
994
995 evTermCoercion :: EvTerm -> TcCoercion
996 -- Applied only to EvTerms of type (s~t)
997 -- See Note [Coercion evidence terms]
998 evTermCoercion (EvId v) = mkTcCoVarCo v
999 evTermCoercion (EvCoercion co) = co
1000 evTermCoercion (EvCast tm co) = TcCastCo (evTermCoercion tm) co
1001 evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
1002
1003 evVarsOfTerm :: EvTerm -> VarSet
1004 evVarsOfTerm (EvId v) = unitVarSet v
1005 evVarsOfTerm (EvCoercion co) = coVarsOfTcCo co
1006 evVarsOfTerm (EvDFunApp _ _ evs) = mkVarSet evs
1007 evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v
1008 evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfTcCo co
1009 evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
1010 evVarsOfTerm (EvLit _) = emptyVarSet
1011 evVarsOfTerm (EvCallStack cs) = evVarsOfCallStack cs
1012 evVarsOfTerm (EvTypeable ev) = evVarsOfTypeable ev
1013
1014 evVarsOfTerms :: [EvTerm] -> VarSet
1015 evVarsOfTerms = mapUnionVarSet evVarsOfTerm
1016
1017 evVarsOfCallStack :: EvCallStack -> VarSet
1018 evVarsOfCallStack cs = case cs of
1019 EvCsEmpty -> emptyVarSet
1020 EvCsTop _ _ tm -> evVarsOfTerm tm
1021 EvCsPushCall _ _ tm -> evVarsOfTerm tm
1022
1023 evVarsOfTypeable :: EvTypeable -> VarSet
1024 evVarsOfTypeable ev =
1025 case ev of
1026 EvTypeableTyCon _ _ -> emptyVarSet
1027 EvTypeableTyApp e1 e2 -> evVarsOfTerms (map fst [e1,e2])
1028 EvTypeableTyLit e -> evVarsOfTerm (fst e)
1029
1030 {-
1031 ************************************************************************
1032 * *
1033 Pretty printing
1034 * *
1035 ************************************************************************
1036 -}
1037
1038 instance Outputable HsWrapper where
1039 ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn
1040
1041 pprHsWrapper :: SDoc -> HsWrapper -> SDoc
1042 -- In debug mode, print the wrapper
1043 -- otherwise just print what's inside
1044 pprHsWrapper doc wrap
1045 = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)
1046 where
1047 help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
1048 -- True <=> appears in function application position
1049 -- False <=> appears as body of let or lambda
1050 help it WpHole = it
1051 help it (WpCompose f1 f2) = help (help it f2) f1
1052 help it (WpFun f1 f2 t1 _) = add_parens $ ptext (sLit "\\(x") <> dcolon <> ppr t1 <> ptext (sLit ").") <+>
1053 help (\_ -> it True <+> help (\_ -> ptext (sLit "x")) f1 True) f2 False
1054 help it (WpCast co) = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")
1055 <+> pprParendTcCo co)]
1056 help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)]
1057 help it (WpTyApp ty) = no_parens $ sep [it True, ptext (sLit "@") <+> pprParendType ty]
1058 help it (WpEvLam id) = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]
1059 help it (WpTyLam tv) = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]
1060 help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]
1061
1062 pp_bndr v = pprBndr LambdaBind v <> dot
1063
1064 add_parens, no_parens :: SDoc -> Bool -> SDoc
1065 add_parens d True = parens d
1066 add_parens d False = d
1067 no_parens d _ = d
1068
1069 instance Outputable TcEvBinds where
1070 ppr (TcEvBinds v) = ppr v
1071 ppr (EvBinds bs) = ptext (sLit "EvBinds") <> braces (vcat (map ppr (bagToList bs)))
1072
1073 instance Outputable EvBindsVar where
1074 ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)
1075
1076 instance Outputable EvBind where
1077 ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
1078 = sep [ pp_gw <+> ppr v
1079 , nest 2 $ equals <+> ppr e ]
1080 where
1081 pp_gw = brackets (if is_given then char 'G' else char 'W')
1082 -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
1083
1084 instance Outputable EvTerm where
1085 ppr (EvId v) = ppr v
1086 ppr (EvCast v co) = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co
1087 ppr (EvCoercion co) = ptext (sLit "CO") <+> ppr co
1088 ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))
1089 ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
1090 ppr (EvLit l) = ppr l
1091 ppr (EvCallStack cs) = ppr cs
1092 ppr (EvDelayedError ty msg) = ptext (sLit "error")
1093 <+> sep [ char '@' <> ppr ty, ppr msg ]
1094 ppr (EvTypeable ev) = ppr ev
1095
1096 instance Outputable EvLit where
1097 ppr (EvNum n) = integer n
1098 ppr (EvStr s) = text (show s)
1099
1100 instance Outputable EvCallStack where
1101 ppr EvCsEmpty
1102 = ptext (sLit "[]")
1103 ppr (EvCsTop name loc tm)
1104 = angleBrackets (ppr (name,loc)) <+> ptext (sLit ":") <+> ppr tm
1105 ppr (EvCsPushCall name loc tm)
1106 = angleBrackets (ppr (name,loc)) <+> ptext (sLit ":") <+> ppr tm
1107
1108 instance Outputable EvTypeable where
1109 ppr ev =
1110 case ev of
1111 EvTypeableTyCon tc ks -> parens (ppr tc <+> sep (map ppr ks))
1112 EvTypeableTyApp t1 t2 -> parens (ppr (fst t1) <+> ppr (fst t2))
1113 EvTypeableTyLit x -> ppr (fst x)
1114
1115
1116 ----------------------------------------------------------------------
1117 -- Helper functions for dealing with IP newtype-dictionaries
1118 ----------------------------------------------------------------------
1119
1120 -- | Create a 'Coercion' that unwraps an implicit-parameter dictionary
1121 -- to expose the underlying value. We expect the 'Type' to have the form
1122 -- `IP sym ty`, return a 'Coercion' `co :: IP sym ty ~ ty`.
1123 unwrapIP :: Type -> Coercion
1124 unwrapIP ty =
1125 case unwrapNewTyCon_maybe tc of
1126 Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys
1127 Nothing -> pprPanic "unwrapIP" $
1128 text "The dictionary for" <+> quotes (ppr tc)
1129 <+> text "is not a newtype!"
1130 where
1131 (tc, tys) = splitTyConApp ty
1132
1133 -- | Create a 'Coercion' that wraps a value in an implicit-parameter
1134 -- dictionary. See 'unwrapIP'.
1135 wrapIP :: Type -> Coercion
1136 wrapIP ty = mkSymCo (unwrapIP ty)