Implememt -fdefer-type-errors (Trac #5624)
[ghc.git] / compiler / typecheck / TcEvidence.lhs
1 %\r
2 % (c) The University of Glasgow 2006\r
3 %\r
4 \r
5 \begin{code}\r
6 module TcEvidence (\r
7 \r
8   -- HsWrapper\r
9   HsWrapper(..), \r
10   (<.>), mkWpTyApps, mkWpEvApps, mkWpEvVarApps, mkWpTyLams, mkWpLams, mkWpLet, \r
11   idHsWrapper, isIdHsWrapper, pprHsWrapper,\r
12 \r
13   -- Evidence bindin\r
14   TcEvBinds(..), EvBindsVar(..), \r
15   EvBindMap(..), emptyEvBindMap, extendEvBinds, lookupEvBind, evBindMapBinds,\r
16 \r
17   EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, \r
18 \r
19   EvTerm(..), mkEvCast, evVarsOfTerm, mkEvKindCast,\r
20 \r
21   -- TcCoercion\r
22   TcCoercion(..), \r
23   mkTcReflCo, mkTcTyConAppCo, mkTcAppCo, mkTcAppCos, mkTcFunCo,\r
24   mkTcAxInstCo, mkTcForAllCo, mkTcForAllCos, \r
25   mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcInstCos,\r
26   tcCoercionKind, coVarsOfTcCo, isEqVar, mkTcCoVarCo, \r
27   isTcReflCo, isTcReflCo_maybe, getTcCoVar_maybe,\r
28   liftTcCoSubstWith\r
29 \r
30   ) where\r
31 #include "HsVersions.h"\r
32 \r
33 import Var\r
34 \r
35 import PprCore ()   -- Instance OutputableBndr TyVar\r
36 import TypeRep  -- Knows type representation\r
37 import TcType\r
38 import Type( tyConAppArgN, getEqPredTys_maybe, tyConAppTyCon_maybe )\r
39 import TysPrim( funTyCon )\r
40 import TyCon\r
41 import PrelNames\r
42 import VarEnv\r
43 import VarSet\r
44 import Name\r
45 \r
46 import Util\r
47 import Bag\r
48 import Pair\r
49 import Control.Applicative\r
50 import Data.Traversable (traverse, sequenceA)\r
51 import qualified Data.Data as Data \r
52 import Outputable\r
53 import FastString\r
54 import Data.IORef( IORef )\r
55 \end{code}\r
56 \r
57 \r
58 Note [TcCoercions]\r
59 ~~~~~~~~~~~~~~~~~~\r
60 | LCoercions are a hack used by the typechecker. Normally,\r
61 Coercions have free variables of type (a ~# b): we call these\r
62 CoVars. However, the type checker passes around equality evidence\r
63 (boxed up) at type (a ~ b).\r
64 \r
65 An LCoercion is simply a Coercion whose free variables have the\r
66 boxed type (a ~ b). After we are done with typechecking the\r
67 desugarer finds the free variables, unboxes them, and creates a\r
68 resulting real Coercion with kosher free variables.\r
69 \r
70 We can use most of the Coercion "smart constructors" to build LCoercions. However,\r
71 mkCoVarCo will not work! The equivalent is mkTcCoVarCo.\r
72 \r
73 The data type is similar to Coercion.Coercion, with the following\r
74 differences\r
75   * Most important, TcLetCo adds let-bindings for coercions.\r
76     This is what lets us unify two for-all types and generate\r
77     equality constraints underneath\r
78 \r
79   * The kind of a TcCoercion is  t1 ~  t2 \r
80              of a Coercion   is  t1 ~# t2\r
81 \r
82   * TcAxiomInstCo takes Types, not Coecions as arguments;\r
83     the generality is required only in the Simplifier\r
84 \r
85   * UnsafeCo aren't required\r
86 \r
87   * Reprsentation invariants are weaker:\r
88      - we are allowed to have type synonyms in TcTyConAppCo\r
89      - the first arg of a TcAppCo can be a TcTyConAppCo\r
90     Reason: they'll get established when we desugar to Coercion\r
91 \r
92 \begin{code}\r
93 data TcCoercion \r
94   = TcRefl TcType\r
95   | TcTyConAppCo TyCon [TcCoercion]\r
96   | TcAppCo TcCoercion TcCoercion\r
97   | TcForAllCo TyVar TcCoercion \r
98   | TcInstCo TcCoercion TcType\r
99   | TcCoVarCo EqVar\r
100   | TcAxiomInstCo CoAxiom [TcType]\r
101   | TcSymCo TcCoercion\r
102   | TcTransCo TcCoercion TcCoercion\r
103   | TcNthCo Int TcCoercion\r
104   | TcLetCo TcEvBinds TcCoercion\r
105   deriving (Data.Data, Data.Typeable)\r
106 \r
107 isEqVar :: Var -> Bool \r
108 -- Is lifted coercion variable (only!)\r
109 isEqVar v = case tyConAppTyCon_maybe (varType v) of\r
110                Just tc -> tc `hasKey` eqTyConKey\r
111                Nothing -> False\r
112 \r
113 isTcReflCo_maybe :: TcCoercion -> Maybe TcType\r
114 isTcReflCo_maybe (TcRefl ty) = Just ty\r
115 isTcReflCo_maybe _             = Nothing\r
116 \r
117 isTcReflCo :: TcCoercion -> Bool\r
118 isTcReflCo (TcRefl {}) = True\r
119 isTcReflCo _           = False\r
120 \r
121 getTcCoVar_maybe :: TcCoercion -> Maybe CoVar\r
122 getTcCoVar_maybe (TcCoVarCo v) = Just v\r
123 getTcCoVar_maybe _             = Nothing\r
124 \r
125 mkTcReflCo :: TcType -> TcCoercion\r
126 mkTcReflCo = TcRefl\r
127 \r
128 mkTcFunCo :: TcCoercion -> TcCoercion -> TcCoercion\r
129 mkTcFunCo co1 co2 = mkTcTyConAppCo funTyCon [co1, co2]\r
130 \r
131 mkTcTyConAppCo :: TyCon -> [TcCoercion] -> TcCoercion\r
132 mkTcTyConAppCo tc cos   -- No need to expand type synonyms\r
133                         -- See Note [TcCoercions]\r
134   | Just tys <- traverse isTcReflCo_maybe cos \r
135   = TcRefl (mkTyConApp tc tys)    -- See Note [Refl invariant]\r
136 \r
137   | otherwise = TcTyConAppCo tc cos\r
138 \r
139 mkTcAxInstCo :: CoAxiom -> [TcType] -> TcCoercion\r
140 mkTcAxInstCo ax tys\r
141   | arity == n_tys = TcAxiomInstCo ax tys\r
142   | otherwise      = ASSERT( arity < n_tys )\r
143                      foldl TcAppCo (TcAxiomInstCo ax (take arity tys))\r
144                                    (map TcRefl (drop arity tys))\r
145   where\r
146     n_tys = length tys\r
147     arity = coAxiomArity ax\r
148 \r
149 mkTcAppCo :: TcCoercion -> TcCoercion -> TcCoercion\r
150 -- No need to deal with TyConApp on the left; see Note [TcCoercions]\r
151 mkTcAppCo (TcRefl ty1) (TcRefl ty2)     = TcRefl (mkAppTy ty1 ty2)\r
152 mkTcAppCo co1 co2                       = TcAppCo co1 co2\r
153 \r
154 mkTcSymCo :: TcCoercion -> TcCoercion\r
155 mkTcSymCo co@(TcRefl {})  = co\r
156 mkTcSymCo    (TcSymCo co) = co\r
157 mkTcSymCo co              = TcSymCo co\r
158 \r
159 mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion\r
160 mkTcTransCo (TcRefl _) co = co\r
161 mkTcTransCo co (TcRefl _) = co\r
162 mkTcTransCo co1 co2       = TcTransCo co1 co2\r
163 \r
164 mkTcNthCo :: Int -> TcCoercion -> TcCoercion\r
165 mkTcNthCo n (TcRefl ty) = TcRefl (tyConAppArgN n ty)\r
166 mkTcNthCo n co          = TcNthCo n co\r
167 \r
168 mkTcAppCos :: TcCoercion -> [TcCoercion] -> TcCoercion\r
169 mkTcAppCos co1 tys = foldl mkTcAppCo co1 tys\r
170 \r
171 mkTcForAllCo :: Var -> TcCoercion -> TcCoercion\r
172 -- note that a TyVar should be used here, not a CoVar (nor a TcTyVar)\r
173 mkTcForAllCo tv (TcRefl ty) = ASSERT( isTyVar tv ) TcRefl (mkForAllTy tv ty)\r
174 mkTcForAllCo tv  co         = ASSERT( isTyVar tv ) TcForAllCo tv co\r
175 \r
176 mkTcForAllCos :: [Var] -> TcCoercion -> TcCoercion\r
177 mkTcForAllCos tvs (TcRefl ty) = ASSERT( all isTyVar tvs ) TcRefl (mkForAllTys tvs ty)\r
178 mkTcForAllCos tvs co          = ASSERT( all isTyVar tvs ) foldr TcForAllCo co tvs\r
179 \r
180 mkTcInstCos :: TcCoercion -> [TcType] -> TcCoercion\r
181 mkTcInstCos (TcRefl ty) tys = TcRefl (applyTys ty tys)\r
182 mkTcInstCos co tys          = foldl TcInstCo co tys\r
183 \r
184 mkTcCoVarCo :: EqVar -> TcCoercion\r
185 -- ipv :: s ~ t  (the boxed equality type)\r
186 mkTcCoVarCo ipv\r
187   | ty1 `eqType` ty2 = TcRefl ty1\r
188   | otherwise        = TcCoVarCo ipv\r
189   where\r
190     (ty1, ty2) = case getEqPredTys_maybe (varType ipv) of\r
191         Nothing  -> pprPanic "mkCoVarLCo" (ppr ipv)\r
192         Just tys -> tys\r
193 \end{code}\r
194 \r
195 \begin{code}\r
196 tcCoercionKind :: TcCoercion -> Pair Type\r
197 tcCoercionKind co = go co \r
198   where \r
199     go (TcRefl ty)            = Pair ty ty\r
200     go (TcLetCo _ co)         = go co\r
201     go (TcTyConAppCo tc cos)  = mkTyConApp tc <$> (sequenceA $ map go cos)\r
202     go (TcAppCo co1 co2)      = mkAppTy <$> go co1 <*> go co2\r
203     go (TcForAllCo tv co)     = mkForAllTy tv <$> go co\r
204     go (TcInstCo co ty)       = go_inst co [ty]\r
205     go (TcCoVarCo cv)         = eqVarKind cv\r
206     go (TcAxiomInstCo ax tys) = Pair (substTyWith (co_ax_tvs ax) tys (co_ax_lhs ax)) \r
207                                      (substTyWith (co_ax_tvs ax) tys (co_ax_rhs ax))\r
208     go (TcSymCo co)           = swap $ go co\r
209     go (TcTransCo co1 co2)    = Pair (pFst $ go co1) (pSnd $ go co2)\r
210     go (TcNthCo d co)         = tyConAppArgN d <$> go co\r
211 \r
212     -- c.f. Coercion.coercionKind\r
213     go_inst (TcInstCo co ty) tys = go_inst co (ty:tys)\r
214     go_inst co               tys = (`applyTys` tys) <$> go co\r
215 \r
216 eqVarKind :: EqVar -> Pair Type\r
217 eqVarKind cv\r
218  | Just (tc, [_kind,ty1,ty2]) <- tcSplitTyConApp_maybe (varType cv)\r
219  = ASSERT (tc `hasKey` eqTyConKey)\r
220    Pair ty1 ty2\r
221  | otherwise = panic "eqVarKind, non coercion variable"\r
222 \r
223 coVarsOfTcCo :: TcCoercion -> VarSet\r
224 -- Only works on *zonked* coercions, because of TcLetCo\r
225 coVarsOfTcCo tc_co\r
226   = go tc_co\r
227   where\r
228     go (TcRefl _)                = emptyVarSet\r
229     go (TcTyConAppCo _ cos)      = foldr (unionVarSet . go) emptyVarSet cos\r
230     go (TcAppCo co1 co2)         = go co1 `unionVarSet` go co2\r
231     go (TcForAllCo _ co)         = go co\r
232     go (TcInstCo co _)           = go co\r
233     go (TcCoVarCo v)             = unitVarSet v\r
234     go (TcAxiomInstCo {})        = emptyVarSet\r
235     go (TcSymCo co)              = go co\r
236     go (TcTransCo co1 co2)       = go co1 `unionVarSet` go co2\r
237     go (TcNthCo _ co)            = go co\r
238     go (TcLetCo (EvBinds bs) co) = foldrBag (unionVarSet . go_bind) (go co) bs\r
239                                    `minusVarSet` get_bndrs bs\r
240     go (TcLetCo {}) = pprPanic "coVarsOfTcCo called on non-zonked TcCoercion" (ppr tc_co)\r
241 \r
242     -- We expect only coercion bindings\r
243     go_bind :: EvBind -> VarSet\r
244     go_bind (EvBind _ (EvCoercion co)) = go co\r
245     go_bind (EvBind _ (EvId v))        = unitVarSet v\r
246     go_bind other = pprPanic "coVarsOfTcCo:Bind" (ppr other)\r
247 \r
248     get_bndrs :: Bag EvBind -> VarSet\r
249     get_bndrs = foldrBag (\ (EvBind b _) bs -> extendVarSet bs b) emptyVarSet \r
250 \r
251 liftTcCoSubstWith :: [TyVar] -> [TcCoercion] -> TcType -> TcCoercion\r
252 -- This version can ignore capture; the free varialbes of the \r
253 -- TcCoerion are all fresh.  Result is mush simpler code\r
254 liftTcCoSubstWith tvs cos ty\r
255   = ASSERT( equalLength tvs cos )\r
256     go ty\r
257   where\r
258     env = zipVarEnv tvs cos\r
259 \r
260     go ty@(TyVarTy tv)   = case lookupVarEnv env tv of\r
261                              Just co -> co\r
262                              Nothing -> mkTcReflCo ty\r
263     go (AppTy t1 t2)     = mkTcAppCo (go t1) (go t2)\r
264     go (TyConApp tc tys) = mkTcTyConAppCo tc (map go tys)\r
265     go (ForAllTy tv ty)  = mkTcForAllCo tv (go ty)\r
266     go (FunTy t1 t2)     = mkTcFunCo (go t1) (go t2)\r
267 \end{code}\r
268 \r
269 Pretty printing\r
270 \r
271 \begin{code}\r
272 instance Outputable TcCoercion where\r
273   ppr = pprTcCo\r
274 \r
275 pprTcCo, pprParendTcCo :: TcCoercion -> SDoc\r
276 pprTcCo       co = ppr_co TopPrec   co\r
277 pprParendTcCo co = ppr_co TyConPrec co\r
278 \r
279 ppr_co :: Prec -> TcCoercion -> SDoc\r
280 ppr_co _ (TcRefl ty) = angleBrackets (ppr ty)\r
281 \r
282 ppr_co p co@(TcTyConAppCo tc [_,_])\r
283   | tc `hasKey` funTyConKey = ppr_fun_co p co\r
284 \r
285 ppr_co p (TcTyConAppCo tc cos)   = pprTcApp   p ppr_co tc cos\r
286 ppr_co p (TcLetCo bs co)         = maybeParen p TopPrec $\r
287                                    sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]\r
288 ppr_co p (TcAppCo co1 co2)       = maybeParen p TyConPrec $\r
289                                    pprTcCo co1 <+> ppr_co TyConPrec co2\r
290 ppr_co p co@(TcForAllCo {})      = ppr_forall_co p co\r
291 ppr_co p (TcInstCo co ty)        = maybeParen p TyConPrec $\r
292                                    pprParendTcCo co <> ptext (sLit "@") <> pprType ty\r
293                      \r
294 ppr_co _ (TcCoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)\r
295 ppr_co p (TcAxiomInstCo con cos) = pprTypeNameApp p ppr_type (getName con) cos\r
296 \r
297 ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $\r
298                                ppr_co FunPrec co1\r
299                                <+> ptext (sLit ";")\r
300                                <+> ppr_co FunPrec co2\r
301 ppr_co p (TcSymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]\r
302 ppr_co p (TcNthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]\r
303 \r
304 ppr_fun_co :: Prec -> TcCoercion -> SDoc\r
305 ppr_fun_co p co = pprArrowChain p (split co)\r
306   where\r
307     split :: TcCoercion -> [SDoc]\r
308     split (TcTyConAppCo f [arg,res])\r
309       | f `hasKey` funTyConKey\r
310       = ppr_co FunPrec arg : split res\r
311     split co = [ppr_co TopPrec co]\r
312 \r
313 ppr_forall_co :: Prec -> TcCoercion -> SDoc\r
314 ppr_forall_co p ty\r
315   = maybeParen p FunPrec $\r
316     sep [pprForAll tvs, ppr_co TopPrec rho]\r
317   where\r
318     (tvs,  rho) = split1 [] ty\r
319     split1 tvs (TcForAllCo tv ty) = split1 (tv:tvs) ty\r
320     split1 tvs ty                 = (reverse tvs, ty)\r
321 \end{code}\r
322 \r
323 %************************************************************************\r
324 %*                                                                      *\r
325                   HsWrapper\r
326 %*                                                                      *\r
327 %************************************************************************\r
328 \r
329 \begin{code}\r
330 data HsWrapper\r
331   = WpHole                      -- The identity coercion\r
332 \r
333   | WpCompose HsWrapper HsWrapper\r
334        -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]\r
335        --\r
336        -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])\r
337        -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)\r
338 \r
339   | WpCast TcCoercion         -- A cast:  [] `cast` co\r
340                               -- Guaranteed not the identity coercion\r
341 \r
342         -- Evidence abstraction and application\r
343         -- (both dictionaries and coercions)\r
344   | WpEvLam EvVar               -- \d. []       the 'd' is an evidence variable\r
345   | WpEvApp EvTerm              -- [] d         the 'd' is evidence for a constraint\r
346 \r
347         -- Kind and Type abstraction and application\r
348   | WpTyLam TyVar       -- \a. []  the 'a' is a type/kind variable (not coercion var)\r
349   | WpTyApp KindOrType  -- [] t    the 't' is a type (not coercion)\r
350 \r
351 \r
352   | WpLet TcEvBinds             -- Non-empty (or possibly non-empty) evidence bindings,\r
353                                 -- so that the identity coercion is always exactly WpHole\r
354   deriving (Data.Data, Data.Typeable)\r
355 \r
356 \r
357 (<.>) :: HsWrapper -> HsWrapper -> HsWrapper\r
358 WpHole <.> c = c\r
359 c <.> WpHole = c\r
360 c1 <.> c2    = c1 `WpCompose` c2\r
361 \r
362 mkWpTyApps :: [Type] -> HsWrapper\r
363 mkWpTyApps tys = mk_co_app_fn WpTyApp tys\r
364 \r
365 mkWpEvApps :: [EvTerm] -> HsWrapper\r
366 mkWpEvApps args = mk_co_app_fn WpEvApp args\r
367 \r
368 mkWpEvVarApps :: [EvVar] -> HsWrapper\r
369 mkWpEvVarApps vs = mkWpEvApps (map EvId vs)\r
370 \r
371 mkWpTyLams :: [TyVar] -> HsWrapper\r
372 mkWpTyLams ids = mk_co_lam_fn WpTyLam ids\r
373 \r
374 mkWpLams :: [Var] -> HsWrapper\r
375 mkWpLams ids = mk_co_lam_fn WpEvLam ids\r
376 \r
377 mkWpLet :: TcEvBinds -> HsWrapper\r
378 -- This no-op is a quite a common case\r
379 mkWpLet (EvBinds b) | isEmptyBag b = WpHole\r
380 mkWpLet ev_binds                   = WpLet ev_binds\r
381 \r
382 mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper\r
383 mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as\r
384 \r
385 mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper\r
386 -- For applications, the *first* argument must\r
387 -- come *last* in the composition sequence\r
388 mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as\r
389 \r
390 idHsWrapper :: HsWrapper\r
391 idHsWrapper = WpHole\r
392 \r
393 isIdHsWrapper :: HsWrapper -> Bool\r
394 isIdHsWrapper WpHole = True\r
395 isIdHsWrapper _      = False\r
396 \end{code}\r
397 \r
398 \r
399 %************************************************************************\r
400 %*                                                                      *\r
401                   Evidence bindings\r
402 %*                                                                      *\r
403 %************************************************************************\r
404 \r
405 \begin{code}\r
406 data TcEvBinds\r
407   = TcEvBinds           -- Mutable evidence bindings\r
408        EvBindsVar       -- Mutable because they are updated "later"\r
409                         --    when an implication constraint is solved\r
410 \r
411   | EvBinds             -- Immutable after zonking\r
412        (Bag EvBind)\r
413 \r
414   deriving( Data.Typeable )\r
415 \r
416 data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique\r
417      -- The Unique is only for debug printing\r
418 \r
419 instance Data.Data TcEvBinds where\r
420   -- Placeholder; we can't travers into TcEvBinds\r
421   toConstr _   = abstractConstr "TcEvBinds"\r
422   gunfold _ _  = error "gunfold"\r
423   dataTypeOf _ = Data.mkNoRepType "TcEvBinds"\r
424 \r
425 -----------------\r
426 newtype EvBindMap \r
427   = EvBindMap { \r
428        ev_bind_varenv :: VarEnv EvBind\r
429     }       -- Map from evidence variables to evidence terms\r
430 \r
431 emptyEvBindMap :: EvBindMap\r
432 emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv }\r
433 \r
434 extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap\r
435 extendEvBinds bs v t \r
436   = EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs) v (EvBind v t) }\r
437 \r
438 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind\r
439 lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs)\r
440 \r
441 evBindMapBinds :: EvBindMap -> Bag EvBind\r
442 evBindMapBinds bs \r
443   = foldVarEnv consBag emptyBag (ev_bind_varenv bs)\r
444 \r
445 -----------------\r
446 -- All evidence is bound by EvBinds; no side effects\r
447 data EvBind = EvBind EvVar EvTerm\r
448 \r
449 data EvTerm\r
450   = EvId EvId                    -- Term-level variable-to-variable bindings\r
451                                  -- (no coercion variables! they come via EvCoercion)\r
452 \r
453   | EvCoercion TcCoercion        -- (Boxed) coercion bindings\r
454 \r
455   | EvCast EvVar TcCoercion      -- d |> co\r
456 \r
457   | EvDFunApp DFunId             -- Dictionary instance application\r
458        [Type] [EvVar]\r
459 \r
460   | EvTupleSel EvId  Int         -- n'th component of the tuple\r
461 \r
462   | EvTupleMk [EvId]             -- tuple built from this stuff\r
463 \r
464   | EvDelayedError Type FastString  -- Used with Opt_DeferTypeErrors\r
465                                -- See Note [Deferring coercion errors to runtime]\r
466                                -- in TcSimplify\r
467 \r
468   | EvSuperClass DictId Int      -- n'th superclass. Used for both equalities and\r
469                                  -- dictionaries, even though the former have no\r
470                                  -- selector Id.  We count up from _0_\r
471   | EvKindCast EvVar TcCoercion  -- See Note [EvKindCast]\r
472            \r
473   deriving( Data.Data, Data.Typeable)\r
474 \end{code}\r
475 \r
476 Note [EvKindCast] \r
477 ~~~~~~~~~~~~~~~~~ \r
478 \r
479 EvKindCast g kco is produced when we have a constraint (g : s1 ~ s2) \r
480 but the kinds of s1 and s2 (k1 and k2 respectively) don't match but \r
481 are rather equal by a coercion. You may think that this coercion will\r
482 always turn out to be ReflCo, so why is this needed? Because sometimes\r
483 we will want to defer kind errors until the runtime and in these cases\r
484 that coercion will be an 'error' term, which we want to evaluate rather\r
485 than silently forget about!\r
486 \r
487 The relevant (and only) place where such a coercion is produced in \r
488 the simplifier is in emit_kind_constraint in TcCanonical.\r
489 \r
490 \r
491 Note [EvBinds/EvTerm]\r
492 ~~~~~~~~~~~~~~~~~~~~~\r
493 How evidence is created and updated. Bindings for dictionaries,\r
494 and coercions and implicit parameters are carried around in TcEvBinds\r
495 which during constraint generation and simplification is always of the\r
496 form (TcEvBinds ref). After constraint simplification is finished it\r
497 will be transformed to t an (EvBinds ev_bag).\r
498 \r
499 Evidence for coercions *SHOULD* be filled in using the TcEvBinds\r
500 However, all EvVars that correspond to *wanted* coercion terms in\r
501 an EvBind must be mutable variables so that they can be readily\r
502 inlined (by zonking) after constraint simplification is finished.\r
503 \r
504 Conclusion: a new wanted coercion variable should be made mutable.\r
505 [Notice though that evidence variables that bind coercion terms\r
506  from super classes will be "given" and hence rigid]\r
507 \r
508 \r
509 \begin{code}\r
510 mkEvCast :: EvVar -> TcCoercion -> EvTerm\r
511 mkEvCast ev lco\r
512   | isTcReflCo lco = EvId ev\r
513   | otherwise      = EvCast ev lco\r
514 \r
515 mkEvKindCast :: EvVar -> TcCoercion -> EvTerm\r
516 mkEvKindCast ev lco\r
517   | isTcReflCo lco = EvId ev\r
518   | otherwise      = EvKindCast ev lco\r
519 \r
520 emptyTcEvBinds :: TcEvBinds\r
521 emptyTcEvBinds = EvBinds emptyBag\r
522 \r
523 isEmptyTcEvBinds :: TcEvBinds -> Bool\r
524 isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b\r
525 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"\r
526 \r
527 \r
528 evVarsOfTerm :: EvTerm -> [EvVar]\r
529 evVarsOfTerm (EvId v) = [v]\r
530 evVarsOfTerm (EvCoercion co)      = varSetElems (coVarsOfTcCo co)\r
531 evVarsOfTerm (EvDFunApp _ _ evs)  = evs\r
532 evVarsOfTerm (EvTupleSel v _)     = [v]\r
533 evVarsOfTerm (EvSuperClass v _)   = [v]\r
534 evVarsOfTerm (EvCast v co)        = v : varSetElems (coVarsOfTcCo co)\r
535 evVarsOfTerm (EvTupleMk evs)      = evs\r
536 evVarsOfTerm (EvDelayedError _ _) = []\r
537 evVarsOfTerm (EvKindCast v co)   = v : varSetElems (coVarsOfTcCo co)\r
538 \end{code}\r
539 \r
540 \r
541 %************************************************************************\r
542 %*                                                                      *\r
543                   Pretty printing\r
544 %*                                                                      *\r
545 %************************************************************************\r
546 \r
547 \begin{code}\r
548 instance Outputable HsWrapper where\r
549   ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn\r
550 \r
551 pprHsWrapper :: SDoc -> HsWrapper -> SDoc\r
552 -- In debug mode, print the wrapper\r
553 -- otherwise just print what's inside\r
554 pprHsWrapper doc wrap\r
555   = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)\r
556   where\r
557     help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc\r
558     -- True  <=> appears in function application position\r
559     -- False <=> appears as body of let or lambda\r
560     help it WpHole             = it\r
561     help it (WpCompose f1 f2)  = help (help it f2) f1\r
562     help it (WpCast co)   = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")\r
563                                               <+> pprParendTcCo co)]\r
564     help it (WpEvApp id)  = no_parens  $ sep [it True, nest 2 (ppr id)]\r
565     help it (WpTyApp ty)  = no_parens  $ sep [it True, ptext (sLit "@") <+> pprParendType ty]\r
566     help it (WpEvLam id)  = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]\r
567     help it (WpTyLam tv)  = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]\r
568     help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]\r
569 \r
570     pp_bndr v = pprBndr LambdaBind v <> dot\r
571 \r
572     add_parens, no_parens :: SDoc -> Bool -> SDoc\r
573     add_parens d True  = parens d\r
574     add_parens d False = d\r
575     no_parens d _ = d\r
576 \r
577 instance Outputable TcEvBinds where\r
578   ppr (TcEvBinds v) = ppr v\r
579   ppr (EvBinds bs)  = ptext (sLit "EvBinds") <> braces (vcat (map ppr (bagToList bs)))\r
580 \r
581 instance Outputable EvBindsVar where\r
582   ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)\r
583 \r
584 instance Outputable EvBind where\r
585   ppr (EvBind v e)   = sep [ ppr v, nest 2 $ equals <+> ppr e ]\r
586    -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing\r
587 \r
588 instance Outputable EvTerm where\r
589   ppr (EvId v)           = ppr v\r
590   ppr (EvCast v co)      = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co\r
591   ppr (EvKindCast v co)  = ppr v <+> (ptext (sLit "`kind-cast`")) <+> pprParendTcCo co\r
592   ppr (EvCoercion co)    = ptext (sLit "CO") <+> ppr co\r
593   ppr (EvTupleSel v n)   = ptext (sLit "tupsel") <> parens (ppr (v,n))\r
594   ppr (EvTupleMk vs)     = ptext (sLit "tupmk") <+> ppr vs\r
595   ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))\r
596   ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]\r
597   ppr (EvDelayedError ty msg) =     ptext (sLit "error") \r
598                                 <+> sep [ char '@' <> ppr ty, ppr msg ]\r
599 \end{code}\r
600 \r