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