Mainly, rename LiteralTy to LitTy
[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 ty@(LitTy {})     = mkTcReflCo ty\r
266     go (ForAllTy tv ty)  = mkTcForAllCo tv (go ty)\r
267     go (FunTy t1 t2)     = mkTcFunCo (go t1) (go t2)\r
268 \end{code}\r
269 \r
270 Pretty printing\r
271 \r
272 \begin{code}\r
273 instance Outputable TcCoercion where\r
274   ppr = pprTcCo\r
275 \r
276 pprTcCo, pprParendTcCo :: TcCoercion -> SDoc\r
277 pprTcCo       co = ppr_co TopPrec   co\r
278 pprParendTcCo co = ppr_co TyConPrec co\r
279 \r
280 ppr_co :: Prec -> TcCoercion -> SDoc\r
281 ppr_co _ (TcRefl ty) = angleBrackets (ppr ty)\r
282 \r
283 ppr_co p co@(TcTyConAppCo tc [_,_])\r
284   | tc `hasKey` funTyConKey = ppr_fun_co p co\r
285 \r
286 ppr_co p (TcTyConAppCo tc cos)   = pprTcApp   p ppr_co tc cos\r
287 ppr_co p (TcLetCo bs co)         = maybeParen p TopPrec $\r
288                                    sep [ptext (sLit "let") <+> braces (ppr bs), ppr co]\r
289 ppr_co p (TcAppCo co1 co2)       = maybeParen p TyConPrec $\r
290                                    pprTcCo co1 <+> ppr_co TyConPrec co2\r
291 ppr_co p co@(TcForAllCo {})      = ppr_forall_co p co\r
292 ppr_co p (TcInstCo co ty)        = maybeParen p TyConPrec $\r
293                                    pprParendTcCo co <> ptext (sLit "@") <> pprType ty\r
294                      \r
295 ppr_co _ (TcCoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)\r
296 ppr_co p (TcAxiomInstCo con cos) = pprTypeNameApp p ppr_type (getName con) cos\r
297 \r
298 ppr_co p (TcTransCo co1 co2) = maybeParen p FunPrec $\r
299                                ppr_co FunPrec co1\r
300                                <+> ptext (sLit ";")\r
301                                <+> ppr_co FunPrec co2\r
302 ppr_co p (TcSymCo co)         = pprPrefixApp p (ptext (sLit "Sym")) [pprParendTcCo co]\r
303 ppr_co p (TcNthCo n co)       = pprPrefixApp p (ptext (sLit "Nth:") <+> int n) [pprParendTcCo co]\r
304 \r
305 ppr_fun_co :: Prec -> TcCoercion -> SDoc\r
306 ppr_fun_co p co = pprArrowChain p (split co)\r
307   where\r
308     split :: TcCoercion -> [SDoc]\r
309     split (TcTyConAppCo f [arg,res])\r
310       | f `hasKey` funTyConKey\r
311       = ppr_co FunPrec arg : split res\r
312     split co = [ppr_co TopPrec co]\r
313 \r
314 ppr_forall_co :: Prec -> TcCoercion -> SDoc\r
315 ppr_forall_co p ty\r
316   = maybeParen p FunPrec $\r
317     sep [pprForAll tvs, ppr_co TopPrec rho]\r
318   where\r
319     (tvs,  rho) = split1 [] ty\r
320     split1 tvs (TcForAllCo tv ty) = split1 (tv:tvs) ty\r
321     split1 tvs ty                 = (reverse tvs, ty)\r
322 \end{code}\r
323 \r
324 %************************************************************************\r
325 %*                                                                      *\r
326                   HsWrapper\r
327 %*                                                                      *\r
328 %************************************************************************\r
329 \r
330 \begin{code}\r
331 data HsWrapper\r
332   = WpHole                      -- The identity coercion\r
333 \r
334   | WpCompose HsWrapper HsWrapper\r
335        -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]\r
336        --\r
337        -- Hence  (\a. []) `WpCompose` (\b. []) = (\a b. [])\r
338        -- But    ([] a)   `WpCompose` ([] b)   = ([] b a)\r
339 \r
340   | WpCast TcCoercion         -- A cast:  [] `cast` co\r
341                               -- Guaranteed not the identity coercion\r
342 \r
343         -- Evidence abstraction and application\r
344         -- (both dictionaries and coercions)\r
345   | WpEvLam EvVar               -- \d. []       the 'd' is an evidence variable\r
346   | WpEvApp EvTerm              -- [] d         the 'd' is evidence for a constraint\r
347 \r
348         -- Kind and Type abstraction and application\r
349   | WpTyLam TyVar       -- \a. []  the 'a' is a type/kind variable (not coercion var)\r
350   | WpTyApp KindOrType  -- [] t    the 't' is a type (not coercion)\r
351 \r
352 \r
353   | WpLet TcEvBinds             -- Non-empty (or possibly non-empty) evidence bindings,\r
354                                 -- so that the identity coercion is always exactly WpHole\r
355   deriving (Data.Data, Data.Typeable)\r
356 \r
357 \r
358 (<.>) :: HsWrapper -> HsWrapper -> HsWrapper\r
359 WpHole <.> c = c\r
360 c <.> WpHole = c\r
361 c1 <.> c2    = c1 `WpCompose` c2\r
362 \r
363 mkWpTyApps :: [Type] -> HsWrapper\r
364 mkWpTyApps tys = mk_co_app_fn WpTyApp tys\r
365 \r
366 mkWpEvApps :: [EvTerm] -> HsWrapper\r
367 mkWpEvApps args = mk_co_app_fn WpEvApp args\r
368 \r
369 mkWpEvVarApps :: [EvVar] -> HsWrapper\r
370 mkWpEvVarApps vs = mkWpEvApps (map EvId vs)\r
371 \r
372 mkWpTyLams :: [TyVar] -> HsWrapper\r
373 mkWpTyLams ids = mk_co_lam_fn WpTyLam ids\r
374 \r
375 mkWpLams :: [Var] -> HsWrapper\r
376 mkWpLams ids = mk_co_lam_fn WpEvLam ids\r
377 \r
378 mkWpLet :: TcEvBinds -> HsWrapper\r
379 -- This no-op is a quite a common case\r
380 mkWpLet (EvBinds b) | isEmptyBag b = WpHole\r
381 mkWpLet ev_binds                   = WpLet ev_binds\r
382 \r
383 mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper\r
384 mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as\r
385 \r
386 mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper\r
387 -- For applications, the *first* argument must\r
388 -- come *last* in the composition sequence\r
389 mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as\r
390 \r
391 idHsWrapper :: HsWrapper\r
392 idHsWrapper = WpHole\r
393 \r
394 isIdHsWrapper :: HsWrapper -> Bool\r
395 isIdHsWrapper WpHole = True\r
396 isIdHsWrapper _      = False\r
397 \end{code}\r
398 \r
399 \r
400 %************************************************************************\r
401 %*                                                                      *\r
402                   Evidence bindings\r
403 %*                                                                      *\r
404 %************************************************************************\r
405 \r
406 \begin{code}\r
407 data TcEvBinds\r
408   = TcEvBinds           -- Mutable evidence bindings\r
409        EvBindsVar       -- Mutable because they are updated "later"\r
410                         --    when an implication constraint is solved\r
411 \r
412   | EvBinds             -- Immutable after zonking\r
413        (Bag EvBind)\r
414 \r
415   deriving( Data.Typeable )\r
416 \r
417 data EvBindsVar = EvBindsVar (IORef EvBindMap) Unique\r
418      -- The Unique is only for debug printing\r
419 \r
420 instance Data.Data TcEvBinds where\r
421   -- Placeholder; we can't travers into TcEvBinds\r
422   toConstr _   = abstractConstr "TcEvBinds"\r
423   gunfold _ _  = error "gunfold"\r
424   dataTypeOf _ = Data.mkNoRepType "TcEvBinds"\r
425 \r
426 -----------------\r
427 newtype EvBindMap \r
428   = EvBindMap { \r
429        ev_bind_varenv :: VarEnv EvBind\r
430     }       -- Map from evidence variables to evidence terms\r
431 \r
432 emptyEvBindMap :: EvBindMap\r
433 emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyVarEnv }\r
434 \r
435 extendEvBinds :: EvBindMap -> EvVar -> EvTerm -> EvBindMap\r
436 extendEvBinds bs v t \r
437   = EvBindMap { ev_bind_varenv = extendVarEnv (ev_bind_varenv bs) v (EvBind v t) }\r
438 \r
439 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind\r
440 lookupEvBind bs = lookupVarEnv (ev_bind_varenv bs)\r
441 \r
442 evBindMapBinds :: EvBindMap -> Bag EvBind\r
443 evBindMapBinds bs \r
444   = foldVarEnv consBag emptyBag (ev_bind_varenv bs)\r
445 \r
446 -----------------\r
447 -- All evidence is bound by EvBinds; no side effects\r
448 data EvBind = EvBind EvVar EvTerm\r
449 \r
450 data EvTerm\r
451   = EvId EvId                    -- Term-level variable-to-variable bindings\r
452                                  -- (no coercion variables! they come via EvCoercion)\r
453 \r
454   | EvCoercion TcCoercion        -- (Boxed) coercion bindings\r
455 \r
456   | EvCast EvVar TcCoercion      -- d |> co\r
457 \r
458   | EvDFunApp DFunId             -- Dictionary instance application\r
459        [Type] [EvVar]\r
460 \r
461   | EvTupleSel EvId  Int         -- n'th component of the tuple\r
462 \r
463   | EvTupleMk [EvId]             -- tuple built from this stuff\r
464 \r
465   | EvSuperClass DictId Int      -- n'th superclass. Used for both equalities and\r
466                                  -- dictionaries, even though the former have no\r
467                                  -- selector Id.  We count up from _0_\r
468   | EvKindCast EvVar TcCoercion  -- See Note [EvKindCast]\r
469 \r
470   | EvInteger Integer            -- The dictionary for class "NatI"\r
471                                  -- Note [EvInteger]\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 Note [EvInteger]\r
510 ~~~~~~~~~~~~~~~~\r
511 A part of the type-level naturals implementation is the class "NatI",\r
512 which provides a "smart" constructor for defining singleton values.\r
513 \r
514 newtype NatS (n :: Nat) = NatS Integer\r
515 \r
516 class NatI n where\r
517   natS :: NatS n\r
518 \r
519 Conceptually, this class has infinitely many instances:\r
520 \r
521 instance NatI 0 where natS = NatS 0\r
522 instance NatI 1 where natS = NatS 1\r
523 instance NatI 2 where natS = NatS 2\r
524 ...\r
525 \r
526 In practice, we solve "NatI" predicates in the type-checker because we can't\r
527 have infinately many instances.  The evidence (aka "dictionary")\r
528 for "NatI n" is of the form "EvInteger n".\r
529 \r
530 We make the following assumptions about dictionaries in GHC:\r
531   1. The "dictionary" for classes with a single method---like NatI---is\r
532      a newtype for the type of the method, so using a evidence amounts\r
533      to a coercion, and\r
534   2. Newtypes use the same representation as their definition types.\r
535 \r
536 So, the evidence for "NatI" is just an integer wrapped in 2 newtypes:\r
537 one to make it into a "NatS" value, and another to make it into "NatI" evidence.\r
538 \r
539 \r
540 \r
541 \begin{code}\r
542 mkEvCast :: EvVar -> TcCoercion -> EvTerm\r
543 mkEvCast ev lco\r
544   | isTcReflCo lco = EvId ev\r
545   | otherwise      = EvCast ev lco\r
546 \r
547 mkEvKindCast :: EvVar -> TcCoercion -> EvTerm\r
548 mkEvKindCast ev lco\r
549   | isTcReflCo lco = EvId ev\r
550   | otherwise      = EvKindCast ev lco\r
551 \r
552 emptyTcEvBinds :: TcEvBinds\r
553 emptyTcEvBinds = EvBinds emptyBag\r
554 \r
555 isEmptyTcEvBinds :: TcEvBinds -> Bool\r
556 isEmptyTcEvBinds (EvBinds b)    = isEmptyBag b\r
557 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"\r
558 \r
559 \r
560 evVarsOfTerm :: EvTerm -> [EvVar]\r
561 evVarsOfTerm (EvId v) = [v]\r
562 evVarsOfTerm (EvCoercion co)     = varSetElems (coVarsOfTcCo co)\r
563 evVarsOfTerm (EvDFunApp _ _ evs) = evs\r
564 evVarsOfTerm (EvTupleSel v _)    = [v]\r
565 evVarsOfTerm (EvSuperClass v _)  = [v]\r
566 evVarsOfTerm (EvCast v co)       = v : varSetElems (coVarsOfTcCo co)\r
567 evVarsOfTerm (EvTupleMk evs)     = evs\r
568 evVarsOfTerm (EvKindCast v co)   = v : varSetElems (coVarsOfTcCo co)\r
569 evVarsOfTerm (EvInteger _)       = []\r
570 \end{code}\r
571 \r
572 \r
573 %************************************************************************\r
574 %*                                                                      *\r
575                   Pretty printing\r
576 %*                                                                      *\r
577 %************************************************************************\r
578 \r
579 \begin{code}\r
580 instance Outputable HsWrapper where\r
581   ppr co_fn = pprHsWrapper (ptext (sLit "<>")) co_fn\r
582 \r
583 pprHsWrapper :: SDoc -> HsWrapper -> SDoc\r
584 -- In debug mode, print the wrapper\r
585 -- otherwise just print what's inside\r
586 pprHsWrapper doc wrap\r
587   = getPprStyle (\ s -> if debugStyle s then (help (add_parens doc) wrap False) else doc)\r
588   where\r
589     help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc\r
590     -- True  <=> appears in function application position\r
591     -- False <=> appears as body of let or lambda\r
592     help it WpHole             = it\r
593     help it (WpCompose f1 f2)  = help (help it f2) f1\r
594     help it (WpCast co)   = add_parens $ sep [it False, nest 2 (ptext (sLit "|>")\r
595                                               <+> pprParendTcCo co)]\r
596     help it (WpEvApp id)  = no_parens  $ sep [it True, nest 2 (ppr id)]\r
597     help it (WpTyApp ty)  = no_parens  $ sep [it True, ptext (sLit "@") <+> pprParendType ty]\r
598     help it (WpEvLam id)  = add_parens $ sep [ ptext (sLit "\\") <> pp_bndr id, it False]\r
599     help it (WpTyLam tv)  = add_parens $ sep [ptext (sLit "/\\") <> pp_bndr tv, it False]\r
600     help it (WpLet binds) = add_parens $ sep [ptext (sLit "let") <+> braces (ppr binds), it False]\r
601 \r
602     pp_bndr v = pprBndr LambdaBind v <> dot\r
603 \r
604     add_parens, no_parens :: SDoc -> Bool -> SDoc\r
605     add_parens d True  = parens d\r
606     add_parens d False = d\r
607     no_parens d _ = d\r
608 \r
609 instance Outputable TcEvBinds where\r
610   ppr (TcEvBinds v) = ppr v\r
611   ppr (EvBinds bs)  = ptext (sLit "EvBinds") <> braces (vcat (map ppr (bagToList bs)))\r
612 \r
613 instance Outputable EvBindsVar where\r
614   ppr (EvBindsVar _ u) = ptext (sLit "EvBindsVar") <> angleBrackets (ppr u)\r
615 \r
616 instance Outputable EvBind where\r
617   ppr (EvBind v e)   = sep [ ppr v, nest 2 $ equals <+> ppr e ]\r
618    -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing\r
619 \r
620 instance Outputable EvTerm where\r
621   ppr (EvId v)           = ppr v\r
622   ppr (EvCast v co)      = ppr v <+> (ptext (sLit "`cast`")) <+> pprParendTcCo co\r
623   ppr (EvKindCast v co)  = ppr v <+> (ptext (sLit "`kind-cast`")) <+> pprParendTcCo co\r
624   ppr (EvCoercion co)    = ptext (sLit "CO") <+> ppr co\r
625   ppr (EvTupleSel v n)   = ptext (sLit "tupsel") <> parens (ppr (v,n))\r
626   ppr (EvTupleMk vs)     = ptext (sLit "tupmk") <+> ppr vs\r
627   ppr (EvSuperClass d n) = ptext (sLit "sc") <> parens (ppr (d,n))\r
628   ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]\r
629   ppr (EvInteger n)      = integer n\r
630 \end{code}\r
631 \r