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