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