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