Type-indexed Typeable
[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,
10 mkWpLams, mkWpLet, mkWpCastN, mkWpCastR, collectHsWrapBinders,
11 mkWpFun, mkWpFuns, idHsWrapper, isIdHsWrapper, pprHsWrapper,
12
13 -- Evidence bindings
14 TcEvBinds(..), EvBindsVar(..),
15 EvBindMap(..), emptyEvBindMap, extendEvBinds,
16 lookupEvBind, evBindMapBinds, foldEvBindMap, isEmptyEvBindMap,
17 EvBind(..), emptyTcEvBinds, isEmptyTcEvBinds, mkGivenEvBind, mkWantedEvBind,
18 sccEvBinds, evBindVar,
19 EvTerm(..), mkEvCast, evVarsOfTerm, mkEvScSelectors,
20 EvLit(..), evTermCoercion,
21 EvCallStack(..),
22 EvTypeable(..),
23
24 -- TcCoercion
25 TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole,
26 Role(..), LeftOrRight(..), pickLR,
27 mkTcReflCo, mkTcNomReflCo, mkTcRepReflCo,
28 mkTcTyConAppCo, mkTcAppCo, mkTcFunCo,
29 mkTcAxInstCo, mkTcUnbranchedAxInstCo, mkTcForAllCo, mkTcForAllCos,
30 mkTcSymCo, mkTcTransCo, mkTcNthCo, mkTcLRCo, mkTcSubCo, maybeTcSubCo,
31 tcDowngradeRole,
32 mkTcAxiomRuleCo, mkTcCoherenceLeftCo, mkTcCoherenceRightCo, mkTcPhantomCo,
33 mkTcKindCo,
34 tcCoercionKind, coVarsOfTcCo,
35 mkTcCoVarCo,
36 isTcReflCo,
37 tcCoercionRole,
38 unwrapIP, wrapIP
39 ) where
40 #include "HsVersions.h"
41
42 import Var
43 import CoAxiom
44 import Coercion
45 import PprCore () -- Instance OutputableBndr TyVar
46 import TcType
47 import Type
48 import TyCon
49 import Class( Class )
50 import PrelNames
51 import DynFlags ( gopt, GeneralFlag(Opt_PrintTypecheckerElaboration) )
52 import VarEnv
53 import VarSet
54 import Name
55 import Pair
56
57 import Util
58 import Bag
59 import Digraph
60 import qualified Data.Data as Data
61 import Outputable
62 import FastString
63 import SrcLoc
64 import Data.IORef( IORef )
65 import UniqFM
66
67 {-
68 Note [TcCoercions]
69 ~~~~~~~~~~~~~~~~~~
70 | TcCoercions are a hack used by the typechecker. Normally,
71 Coercions have free variables of type (a ~# b): we call these
72 CoVars. However, the type checker passes around equality evidence
73 (boxed up) at type (a ~ b).
74
75 An TcCoercion is simply a Coercion whose free variables have may be either
76 boxed or unboxed. After we are done with typechecking the desugarer finds the
77 boxed free variables, unboxes them, and creates a resulting real Coercion with
78 kosher free variables.
79
80 -}
81
82 type TcCoercion = Coercion
83 type TcCoercionN = CoercionN -- A Nominal coercion ~N
84 type TcCoercionR = CoercionR -- A Representational coercion ~R
85 type TcCoercionP = CoercionP -- a phantom coercion
86
87 mkTcReflCo :: Role -> TcType -> TcCoercion
88 mkTcSymCo :: TcCoercion -> TcCoercion
89 mkTcTransCo :: TcCoercion -> TcCoercion -> TcCoercion
90 mkTcNomReflCo :: TcType -> TcCoercionN
91 mkTcRepReflCo :: TcType -> TcCoercionR
92 mkTcTyConAppCo :: Role -> TyCon -> [TcCoercion] -> TcCoercion
93 mkTcAppCo :: TcCoercion -> TcCoercionN -> TcCoercion
94 mkTcFunCo :: Role -> TcCoercion -> TcCoercion -> TcCoercion
95 mkTcAxInstCo :: Role -> CoAxiom br -> BranchIndex
96 -> [TcType] -> [TcCoercion] -> TcCoercion
97 mkTcUnbranchedAxInstCo :: CoAxiom Unbranched -> [TcType]
98 -> [TcCoercion] -> TcCoercionR
99 mkTcForAllCo :: TyVar -> TcCoercionN -> TcCoercion -> TcCoercion
100 mkTcForAllCos :: [(TyVar, TcCoercionN)] -> TcCoercion -> TcCoercion
101 mkTcNthCo :: Int -> TcCoercion -> TcCoercion
102 mkTcLRCo :: LeftOrRight -> TcCoercion -> TcCoercion
103 mkTcSubCo :: TcCoercionN -> TcCoercionR
104 maybeTcSubCo :: EqRel -> TcCoercion -> TcCoercion
105 tcDowngradeRole :: Role -> Role -> TcCoercion -> TcCoercion
106 mkTcAxiomRuleCo :: CoAxiomRule -> [TcCoercion] -> TcCoercionR
107 mkTcCoherenceLeftCo :: TcCoercion -> TcCoercionN -> TcCoercion
108 mkTcCoherenceRightCo :: TcCoercion -> TcCoercionN -> TcCoercion
109 mkTcPhantomCo :: TcCoercionN -> TcType -> TcType -> TcCoercionP
110 mkTcKindCo :: TcCoercion -> TcCoercionN
111 mkTcCoVarCo :: CoVar -> TcCoercion
112
113 tcCoercionKind :: TcCoercion -> Pair TcType
114 tcCoercionRole :: TcCoercion -> Role
115 coVarsOfTcCo :: TcCoercion -> TcTyCoVarSet
116 isTcReflCo :: TcCoercion -> Bool
117
118 mkTcReflCo = mkReflCo
119 mkTcSymCo = mkSymCo
120 mkTcTransCo = mkTransCo
121 mkTcNomReflCo = mkNomReflCo
122 mkTcRepReflCo = mkRepReflCo
123 mkTcTyConAppCo = mkTyConAppCo
124 mkTcAppCo = mkAppCo
125 mkTcFunCo = mkFunCo
126 mkTcAxInstCo = mkAxInstCo
127 mkTcUnbranchedAxInstCo = mkUnbranchedAxInstCo Representational
128 mkTcForAllCo = mkForAllCo
129 mkTcForAllCos = mkForAllCos
130 mkTcNthCo = mkNthCo
131 mkTcLRCo = mkLRCo
132 mkTcSubCo = mkSubCo
133 maybeTcSubCo = maybeSubCo
134 tcDowngradeRole = downgradeRole
135 mkTcAxiomRuleCo = mkAxiomRuleCo
136 mkTcCoherenceLeftCo = mkCoherenceLeftCo
137 mkTcCoherenceRightCo = mkCoherenceRightCo
138 mkTcPhantomCo = mkPhantomCo
139 mkTcKindCo = mkKindCo
140 mkTcCoVarCo = mkCoVarCo
141
142 tcCoercionKind = coercionKind
143 tcCoercionRole = coercionRole
144 coVarsOfTcCo = coVarsOfCo
145 isTcReflCo = isReflCo
146
147
148 {-
149 %************************************************************************
150 %* *
151 HsWrapper
152 * *
153 ************************************************************************
154 -}
155
156 data HsWrapper
157 = WpHole -- The identity coercion
158
159 | WpCompose HsWrapper HsWrapper
160 -- (wrap1 `WpCompose` wrap2)[e] = wrap1[ wrap2[ e ]]
161 --
162 -- Hence (\a. []) `WpCompose` (\b. []) = (\a b. [])
163 -- But ([] a) `WpCompose` ([] b) = ([] b a)
164
165 | WpFun HsWrapper HsWrapper TcType SDoc
166 -- (WpFun wrap1 wrap2 t1)[e] = \(x:t1). wrap2[ e wrap1[x] ]
167 -- So note that if wrap1 :: exp_arg <= act_arg
168 -- wrap2 :: act_res <= exp_res
169 -- then WpFun wrap1 wrap2 : (act_arg -> arg_res) <= (exp_arg -> exp_res)
170 -- This isn't the same as for mkFunCo, but it has to be this way
171 -- because we can't use 'sym' to flip around these HsWrappers
172 -- The TcType is the "from" type of the first wrapper
173 -- The SDoc explains the circumstances under which we have created this
174 -- WpFun, in case we run afoul of levity polymorphism restrictions in
175 -- the desugarer. See Note [Levity polymorphism checking] in DsMonad
176
177 | WpCast TcCoercionR -- A cast: [] `cast` co
178 -- Guaranteed not the identity coercion
179 -- At role Representational
180
181 -- Evidence abstraction and application
182 -- (both dictionaries and coercions)
183 | WpEvLam EvVar -- \d. [] the 'd' is an evidence variable
184 | WpEvApp EvTerm -- [] d the 'd' is evidence for a constraint
185 -- Kind and Type abstraction and application
186 | WpTyLam TyVar -- \a. [] the 'a' is a type/kind variable (not coercion var)
187 | WpTyApp KindOrType -- [] t the 't' is a type (not coercion)
188
189
190 | WpLet TcEvBinds -- Non-empty (or possibly non-empty) evidence bindings,
191 -- so that the identity coercion is always exactly WpHole
192
193 -- Cannot derive Data instance because SDoc is not Data (it stores a function).
194 -- So we do it manually:
195 instance Data.Data HsWrapper where
196 gfoldl _ z WpHole = z WpHole
197 gfoldl k z (WpCompose a1 a2) = z WpCompose `k` a1 `k` a2
198 gfoldl k z (WpFun a1 a2 a3 _) = z wpFunEmpty `k` a1 `k` a2 `k` a3
199 gfoldl k z (WpCast a1) = z WpCast `k` a1
200 gfoldl k z (WpEvLam a1) = z WpEvLam `k` a1
201 gfoldl k z (WpEvApp a1) = z WpEvApp `k` a1
202 gfoldl k z (WpTyLam a1) = z WpTyLam `k` a1
203 gfoldl k z (WpTyApp a1) = z WpTyApp `k` a1
204 gfoldl k z (WpLet a1) = z WpLet `k` a1
205
206 gunfold k z c = case Data.constrIndex c of
207 1 -> z WpHole
208 2 -> k (k (z WpCompose))
209 3 -> k (k (k (z wpFunEmpty)))
210 4 -> k (z WpCast)
211 5 -> k (z WpEvLam)
212 6 -> k (z WpEvApp)
213 7 -> k (z WpTyLam)
214 8 -> k (z WpTyApp)
215 _ -> k (z WpLet)
216
217 toConstr WpHole = wpHole_constr
218 toConstr (WpCompose _ _) = wpCompose_constr
219 toConstr (WpFun _ _ _ _) = wpFun_constr
220 toConstr (WpCast _) = wpCast_constr
221 toConstr (WpEvLam _) = wpEvLam_constr
222 toConstr (WpEvApp _) = wpEvApp_constr
223 toConstr (WpTyLam _) = wpTyLam_constr
224 toConstr (WpTyApp _) = wpTyApp_constr
225 toConstr (WpLet _) = wpLet_constr
226
227 dataTypeOf _ = hsWrapper_dataType
228
229 hsWrapper_dataType :: Data.DataType
230 hsWrapper_dataType
231 = Data.mkDataType "HsWrapper"
232 [ wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr
233 , wpEvLam_constr, wpEvApp_constr, wpTyLam_constr, wpTyApp_constr
234 , wpLet_constr]
235
236 wpHole_constr, wpCompose_constr, wpFun_constr, wpCast_constr, wpEvLam_constr,
237 wpEvApp_constr, wpTyLam_constr, wpTyApp_constr, wpLet_constr :: Data.Constr
238 wpHole_constr = mkHsWrapperConstr "WpHole"
239 wpCompose_constr = mkHsWrapperConstr "WpCompose"
240 wpFun_constr = mkHsWrapperConstr "WpFun"
241 wpCast_constr = mkHsWrapperConstr "WpCast"
242 wpEvLam_constr = mkHsWrapperConstr "WpEvLam"
243 wpEvApp_constr = mkHsWrapperConstr "WpEvApp"
244 wpTyLam_constr = mkHsWrapperConstr "WpTyLam"
245 wpTyApp_constr = mkHsWrapperConstr "WpTyApp"
246 wpLet_constr = mkHsWrapperConstr "WpLet"
247
248 mkHsWrapperConstr :: String -> Data.Constr
249 mkHsWrapperConstr name = Data.mkConstr hsWrapper_dataType name [] Data.Prefix
250
251 wpFunEmpty :: HsWrapper -> HsWrapper -> TcType -> HsWrapper
252 wpFunEmpty c1 c2 t1 = WpFun c1 c2 t1 empty
253
254 (<.>) :: HsWrapper -> HsWrapper -> HsWrapper
255 WpHole <.> c = c
256 c <.> WpHole = c
257 c1 <.> c2 = c1 `WpCompose` c2
258
259 mkWpFun :: HsWrapper -> HsWrapper
260 -> TcType -- the "from" type of the first wrapper
261 -> TcType -- either type of the second wrapper (used only when the
262 -- second wrapper is the identity)
263 -> SDoc -- what caused you to want a WpFun? Something like "When converting ..."
264 -> HsWrapper
265 mkWpFun WpHole WpHole _ _ _ = WpHole
266 mkWpFun WpHole (WpCast co2) t1 _ _ = WpCast (mkTcFunCo Representational (mkTcRepReflCo t1) co2)
267 mkWpFun (WpCast co1) WpHole _ t2 _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) (mkTcRepReflCo t2))
268 mkWpFun (WpCast co1) (WpCast co2) _ _ _ = WpCast (mkTcFunCo Representational (mkTcSymCo co1) co2)
269 mkWpFun co1 co2 t1 _ d = WpFun co1 co2 t1 d
270
271 -- | @mkWpFuns [(ty1, wrap1), (ty2, wrap2)] ty_res wrap_res@,
272 -- where @wrap1 :: ty1 "->" ty1'@ and @wrap2 :: ty2 "->" ty2'@,
273 -- @wrap3 :: ty3 "->" ty3'@ and @ty_res@ is /either/ @ty3@ or @ty3'@,
274 -- gives a wrapper @(ty1' -> ty2' -> ty3) "->" (ty1 -> ty2 -> ty3')@.
275 -- Notice that the result wrapper goes the other way round to all
276 -- the others. This is a result of sub-typing contravariance.
277 -- The SDoc is a description of what you were doing when you called mkWpFuns.
278 mkWpFuns :: [(TcType, HsWrapper)] -> TcType -> HsWrapper -> SDoc -> HsWrapper
279 mkWpFuns args res_ty res_wrap doc = snd $ go args res_ty res_wrap
280 where
281 go [] res_ty res_wrap = (res_ty, res_wrap)
282 go ((arg_ty, arg_wrap) : args) res_ty res_wrap
283 = let (tail_ty, tail_wrap) = go args res_ty res_wrap in
284 (arg_ty `mkFunTy` tail_ty, mkWpFun arg_wrap tail_wrap arg_ty tail_ty doc)
285
286 mkWpCastR :: TcCoercionR -> HsWrapper
287 mkWpCastR co
288 | isTcReflCo co = WpHole
289 | otherwise = ASSERT2(tcCoercionRole co == Representational, ppr co)
290 WpCast co
291
292 mkWpCastN :: TcCoercionN -> HsWrapper
293 mkWpCastN co
294 | isTcReflCo co = WpHole
295 | otherwise = ASSERT2(tcCoercionRole co == Nominal, ppr co)
296 WpCast (mkTcSubCo co)
297 -- The mkTcSubCo converts Nominal to Representational
298
299 mkWpTyApps :: [Type] -> HsWrapper
300 mkWpTyApps tys = mk_co_app_fn WpTyApp tys
301
302 mkWpEvApps :: [EvTerm] -> HsWrapper
303 mkWpEvApps args = mk_co_app_fn WpEvApp args
304
305 mkWpEvVarApps :: [EvVar] -> HsWrapper
306 mkWpEvVarApps vs = mk_co_app_fn WpEvApp (map EvId vs)
307
308 mkWpTyLams :: [TyVar] -> HsWrapper
309 mkWpTyLams ids = mk_co_lam_fn WpTyLam ids
310
311 mkWpLams :: [Var] -> HsWrapper
312 mkWpLams ids = mk_co_lam_fn WpEvLam ids
313
314 mkWpLet :: TcEvBinds -> HsWrapper
315 -- This no-op is a quite a common case
316 mkWpLet (EvBinds b) | isEmptyBag b = WpHole
317 mkWpLet ev_binds = WpLet ev_binds
318
319 mk_co_lam_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
320 mk_co_lam_fn f as = foldr (\x wrap -> f x <.> wrap) WpHole as
321
322 mk_co_app_fn :: (a -> HsWrapper) -> [a] -> HsWrapper
323 -- For applications, the *first* argument must
324 -- come *last* in the composition sequence
325 mk_co_app_fn f as = foldr (\x wrap -> wrap <.> f x) WpHole as
326
327 idHsWrapper :: HsWrapper
328 idHsWrapper = WpHole
329
330 isIdHsWrapper :: HsWrapper -> Bool
331 isIdHsWrapper WpHole = True
332 isIdHsWrapper _ = False
333
334 collectHsWrapBinders :: HsWrapper -> ([Var], HsWrapper)
335 -- Collect the outer lambda binders of a HsWrapper,
336 -- stopping as soon as you get to a non-lambda binder
337 collectHsWrapBinders wrap = go wrap []
338 where
339 -- go w ws = collectHsWrapBinders (w <.> w1 <.> ... <.> wn)
340 go :: HsWrapper -> [HsWrapper] -> ([Var], HsWrapper)
341 go (WpEvLam v) wraps = add_lam v (gos wraps)
342 go (WpTyLam v) wraps = add_lam v (gos wraps)
343 go (WpCompose w1 w2) wraps = go w1 (w2:wraps)
344 go wrap wraps = ([], foldl (<.>) wrap wraps)
345
346 gos [] = ([], WpHole)
347 gos (w:ws) = go w ws
348
349 add_lam v (vs,w) = (v:vs, w)
350
351 {-
352 ************************************************************************
353 * *
354 Evidence bindings
355 * *
356 ************************************************************************
357 -}
358
359 data TcEvBinds
360 = TcEvBinds -- Mutable evidence bindings
361 EvBindsVar -- Mutable because they are updated "later"
362 -- when an implication constraint is solved
363
364 | EvBinds -- Immutable after zonking
365 (Bag EvBind)
366
367 data EvBindsVar
368 = EvBindsVar {
369 ebv_uniq :: Unique,
370 -- The Unique is for debug printing only
371
372 ebv_binds :: IORef EvBindMap,
373 -- The main payload: the value-level evidence bindings
374 -- (dictionaries etc)
375
376 ebv_tcvs :: IORef CoVarSet
377 -- The free coercion vars of the (rhss of) the coercion bindings
378 --
379 -- Coercions don't actually have bindings
380 -- because we plug them in-place (via a mutable
381 -- variable); but we keep their free variables
382 -- so that we can report unused given constraints
383 -- See Note [Tracking redundant constraints] in TcSimplify
384 }
385
386 instance Data.Data TcEvBinds where
387 -- Placeholder; we can't travers into TcEvBinds
388 toConstr _ = abstractConstr "TcEvBinds"
389 gunfold _ _ = error "gunfold"
390 dataTypeOf _ = Data.mkNoRepType "TcEvBinds"
391
392 -----------------
393 newtype EvBindMap
394 = EvBindMap {
395 ev_bind_varenv :: DVarEnv EvBind
396 } -- Map from evidence variables to evidence terms
397 -- We use @DVarEnv@ here to get deterministic ordering when we
398 -- turn it into a Bag.
399 -- If we don't do that, when we generate let bindings for
400 -- dictionaries in dsTcEvBinds they will be generated in random
401 -- order.
402 --
403 -- For example:
404 --
405 -- let $dEq = GHC.Classes.$fEqInt in
406 -- let $$dNum = GHC.Num.$fNumInt in ...
407 --
408 -- vs
409 --
410 -- let $dNum = GHC.Num.$fNumInt in
411 -- let $dEq = GHC.Classes.$fEqInt in ...
412 --
413 -- See Note [Deterministic UniqFM] in UniqDFM for explanation why
414 -- @UniqFM@ can lead to nondeterministic order.
415
416 emptyEvBindMap :: EvBindMap
417 emptyEvBindMap = EvBindMap { ev_bind_varenv = emptyDVarEnv }
418
419 extendEvBinds :: EvBindMap -> EvBind -> EvBindMap
420 extendEvBinds bs ev_bind
421 = EvBindMap { ev_bind_varenv = extendDVarEnv (ev_bind_varenv bs)
422 (eb_lhs ev_bind)
423 ev_bind }
424
425 isEmptyEvBindMap :: EvBindMap -> Bool
426 isEmptyEvBindMap (EvBindMap m) = isEmptyDVarEnv m
427
428 lookupEvBind :: EvBindMap -> EvVar -> Maybe EvBind
429 lookupEvBind bs = lookupDVarEnv (ev_bind_varenv bs)
430
431 evBindMapBinds :: EvBindMap -> Bag EvBind
432 evBindMapBinds = foldEvBindMap consBag emptyBag
433
434 foldEvBindMap :: (EvBind -> a -> a) -> a -> EvBindMap -> a
435 foldEvBindMap k z bs = foldDVarEnv k z (ev_bind_varenv bs)
436
437 instance Outputable EvBindMap where
438 ppr (EvBindMap m) = ppr m
439
440 -----------------
441 -- All evidence is bound by EvBinds; no side effects
442 data EvBind
443 = EvBind { eb_lhs :: EvVar
444 , eb_rhs :: EvTerm
445 , eb_is_given :: Bool -- True <=> given
446 -- See Note [Tracking redundant constraints] in TcSimplify
447 }
448
449 evBindVar :: EvBind -> EvVar
450 evBindVar = eb_lhs
451
452 mkWantedEvBind :: EvVar -> EvTerm -> EvBind
453 mkWantedEvBind ev tm = EvBind { eb_is_given = False, eb_lhs = ev, eb_rhs = tm }
454
455
456 mkGivenEvBind :: EvVar -> EvTerm -> EvBind
457 mkGivenEvBind ev tm = EvBind { eb_is_given = True, eb_lhs = ev, eb_rhs = tm }
458
459 data EvTerm
460 = EvId EvId -- Any sort of evidence Id, including coercions
461
462 | EvCoercion TcCoercion -- coercion bindings
463 -- See Note [Coercion evidence terms]
464
465 | EvCast EvTerm TcCoercionR -- d |> co
466
467 | EvDFunApp DFunId -- Dictionary instance application
468 [Type] [EvTerm]
469
470 | EvDelayedError Type FastString -- Used with Opt_DeferTypeErrors
471 -- See Note [Deferring coercion errors to runtime]
472 -- in TcSimplify
473
474 | EvSuperClass EvTerm Int -- n'th superclass. Used for both equalities and
475 -- dictionaries, even though the former have no
476 -- selector Id. We count up from _0_
477
478 | EvLit EvLit -- Dictionary for KnownNat and KnownSymbol classes.
479 -- Note [KnownNat & KnownSymbol and EvLit]
480
481 | EvCallStack EvCallStack -- Dictionary for CallStack implicit parameters
482
483 | EvTypeable Type EvTypeable -- Dictionary for (Typeable ty)
484
485 | EvSelector Id [Type] [EvTerm] -- Selector id plus the types at which it
486 -- should be instantiated, used for HasField
487 -- dictionaries; see Note [HasField instances]
488 -- in TcInterface
489
490 deriving Data.Data
491
492
493 -- | Instructions on how to make a 'Typeable' dictionary.
494 -- See Note [Typeable evidence terms]
495 data EvTypeable
496 = EvTypeableTyCon TyCon [EvTerm]
497 -- ^ Dictionary for @Typeable T@ where @T@ is a type constructor with all of
498 -- its kind variables saturated. The @[EvTerm]@ is @Typeable@ evidence for
499 -- the applied kinds..
500
501 | EvTypeableTyApp EvTerm EvTerm
502 -- ^ Dictionary for @Typeable (s t)@,
503 -- given a dictionaries for @s@ and @t@.
504
505 | EvTypeableTrFun EvTerm EvTerm
506 -- ^ Dictionary for @Typeable (s -> t)@,
507 -- given a dictionaries for @s@ and @t@.
508
509 | EvTypeableTyLit EvTerm
510 -- ^ Dictionary for a type literal,
511 -- e.g. @Typeable "foo"@ or @Typeable 3@
512 -- The 'EvTerm' is evidence of, e.g., @KnownNat 3@
513 -- (see Trac #10348)
514 deriving Data.Data
515
516 data EvLit
517 = EvNum Integer
518 | EvStr FastString
519 deriving Data.Data
520
521 -- | Evidence for @CallStack@ implicit parameters.
522 data EvCallStack
523 -- See Note [Overview of implicit CallStacks]
524 = EvCsEmpty
525 | EvCsPushCall Name RealSrcSpan EvTerm
526 -- ^ @EvCsPushCall name loc stk@ represents a call to @name@, occurring at
527 -- @loc@, in a calling context @stk@.
528 deriving Data.Data
529
530 {-
531 Note [Typeable evidence terms]
532 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
533 The EvTypeable data type looks isomorphic to Type, but the EvTerms
534 inside can be EvIds. Eg
535 f :: forall a. Typeable a => a -> TypeRep
536 f x = typeRep (undefined :: Proxy [a])
537 Here for the (Typeable [a]) dictionary passed to typeRep we make
538 evidence
539 dl :: Typeable [a] = EvTypeable [a]
540 (EvTypeableTyApp (EvTypeableTyCon []) (EvId d))
541 where
542 d :: Typable a
543 is the lambda-bound dictionary passed into f.
544
545 Note [Coercion evidence terms]
546 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
547 A "coercion evidence term" takes one of these forms
548 co_tm ::= EvId v where v :: t1 ~# t2
549 | EvCoercion co
550 | EvCast co_tm co
551
552 We do quite often need to get a TcCoercion from an EvTerm; see
553 'evTermCoercion'.
554
555 INVARIANT: The evidence for any constraint with type (t1 ~# t2) is
556 a coercion evidence term. Consider for example
557 [G] d :: F Int a
558 If we have
559 ax7 a :: F Int a ~ (a ~ Bool)
560 then we do NOT generate the constraint
561 [G] (d |> ax7 a) :: a ~ Bool
562 because that does not satisfy the invariant (d is not a coercion variable).
563 Instead we make a binding
564 g1 :: a~Bool = g |> ax7 a
565 and the constraint
566 [G] g1 :: a~Bool
567 See Trac [7238] and Note [Bind new Givens immediately] in TcRnTypes
568
569 Note [EvBinds/EvTerm]
570 ~~~~~~~~~~~~~~~~~~~~~
571 How evidence is created and updated. Bindings for dictionaries,
572 and coercions and implicit parameters are carried around in TcEvBinds
573 which during constraint generation and simplification is always of the
574 form (TcEvBinds ref). After constraint simplification is finished it
575 will be transformed to t an (EvBinds ev_bag).
576
577 Evidence for coercions *SHOULD* be filled in using the TcEvBinds
578 However, all EvVars that correspond to *wanted* coercion terms in
579 an EvBind must be mutable variables so that they can be readily
580 inlined (by zonking) after constraint simplification is finished.
581
582 Conclusion: a new wanted coercion variable should be made mutable.
583 [Notice though that evidence variables that bind coercion terms
584 from super classes will be "given" and hence rigid]
585
586
587 Note [KnownNat & KnownSymbol and EvLit]
588 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
589 A part of the type-level literals implementation are the classes
590 "KnownNat" and "KnownSymbol", which provide a "smart" constructor for
591 defining singleton values. Here is the key stuff from GHC.TypeLits
592
593 class KnownNat (n :: Nat) where
594 natSing :: SNat n
595
596 newtype SNat (n :: Nat) = SNat Integer
597
598 Conceptually, this class has infinitely many instances:
599
600 instance KnownNat 0 where natSing = SNat 0
601 instance KnownNat 1 where natSing = SNat 1
602 instance KnownNat 2 where natSing = SNat 2
603 ...
604
605 In practice, we solve `KnownNat` predicates in the type-checker
606 (see typecheck/TcInteract.hs) because we can't have infinitely many instances.
607 The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
608
609 We make the following assumptions about dictionaries in GHC:
610 1. The "dictionary" for classes with a single method---like `KnownNat`---is
611 a newtype for the type of the method, so using a evidence amounts
612 to a coercion, and
613 2. Newtypes use the same representation as their definition types.
614
615 So, the evidence for `KnownNat` is just a value of the representation type,
616 wrapped in two newtype constructors: one to make it into a `SNat` value,
617 and another to make it into a `KnownNat` dictionary.
618
619 Also note that `natSing` and `SNat` are never actually exposed from the
620 library---they are just an implementation detail. Instead, users see
621 a more convenient function, defined in terms of `natSing`:
622
623 natVal :: KnownNat n => proxy n -> Integer
624
625 The reason we don't use this directly in the class is that it is simpler
626 and more efficient to pass around an integer rather than an entier function,
627 especially when the `KnowNat` evidence is packaged up in an existential.
628
629 The story for kind `Symbol` is analogous:
630 * class KnownSymbol
631 * newtype SSymbol
632 * Evidence: EvLit (EvStr n)
633
634
635 Note [Overview of implicit CallStacks]
636 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
637 (See https://ghc.haskell.org/trac/ghc/wiki/ExplicitCallStack/ImplicitLocations)
638
639 The goal of CallStack evidence terms is to reify locations
640 in the program source as runtime values, without any support
641 from the RTS. We accomplish this by assigning a special meaning
642 to constraints of type GHC.Stack.Types.HasCallStack, an alias
643
644 type HasCallStack = (?callStack :: CallStack)
645
646 Implicit parameters of type GHC.Stack.Types.CallStack (the name is not
647 important) are solved in three steps:
648
649 1. Occurrences of CallStack IPs are solved directly from the given IP,
650 just like a regular IP. For example, the occurrence of `?stk` in
651
652 error :: (?stk :: CallStack) => String -> a
653 error s = raise (ErrorCall (s ++ prettyCallStack ?stk))
654
655 will be solved for the `?stk` in `error`s context as before.
656
657 2. In a function call, instead of simply passing the given IP, we first
658 append the current call-site to it. For example, consider a
659 call to the callstack-aware `error` above.
660
661 undefined :: (?stk :: CallStack) => a
662 undefined = error "undefined!"
663
664 Here we want to take the given `?stk` and append the current
665 call-site, before passing it to `error`. In essence, we want to
666 rewrite `error "undefined!"` to
667
668 let ?stk = pushCallStack <error's location> ?stk
669 in error "undefined!"
670
671 We achieve this effect by emitting a NEW wanted
672
673 [W] d :: IP "stk" CallStack
674
675 from which we build the evidence term
676
677 EvCsPushCall "error" <error's location> (EvId d)
678
679 that we use to solve the call to `error`. The new wanted `d` will
680 then be solved per rule (1), ie as a regular IP.
681
682 (see TcInteract.interactDict)
683
684 3. We default any insoluble CallStacks to the empty CallStack. Suppose
685 `undefined` did not request a CallStack, ie
686
687 undefinedNoStk :: a
688 undefinedNoStk = error "undefined!"
689
690 Under the usual IP rules, the new wanted from rule (2) would be
691 insoluble as there's no given IP from which to solve it, so we
692 would get an "unbound implicit parameter" error.
693
694 We don't ever want to emit an insoluble CallStack IP, so we add a
695 defaulting pass to default any remaining wanted CallStacks to the
696 empty CallStack with the evidence term
697
698 EvCsEmpty
699
700 (see TcSimplify.simpl_top and TcSimplify.defaultCallStacks)
701
702 This provides a lightweight mechanism for building up call-stacks
703 explicitly, but is notably limited by the fact that the stack will
704 stop at the first function whose type does not include a CallStack IP.
705 For example, using the above definition of `undefined`:
706
707 head :: [a] -> a
708 head [] = undefined
709 head (x:_) = x
710
711 g = head []
712
713 the resulting CallStack will include the call to `undefined` in `head`
714 and the call to `error` in `undefined`, but *not* the call to `head`
715 in `g`, because `head` did not explicitly request a CallStack.
716
717
718 Important Details:
719 - GHC should NEVER report an insoluble CallStack constraint.
720
721 - GHC should NEVER infer a CallStack constraint unless one was requested
722 with a partial type signature (See TcType.pickQuantifiablePreds).
723
724 - A CallStack (defined in GHC.Stack.Types) is a [(String, SrcLoc)],
725 where the String is the name of the binder that is used at the
726 SrcLoc. SrcLoc is also defined in GHC.Stack.Types and contains the
727 package/module/file name, as well as the full source-span. Both
728 CallStack and SrcLoc are kept abstract so only GHC can construct new
729 values.
730
731 - We will automatically solve any wanted CallStack regardless of the
732 name of the IP, i.e.
733
734 f = show (?stk :: CallStack)
735 g = show (?loc :: CallStack)
736
737 are both valid. However, we will only push new SrcLocs onto existing
738 CallStacks when the IP names match, e.g. in
739
740 head :: (?loc :: CallStack) => [a] -> a
741 head [] = error (show (?stk :: CallStack))
742
743 the printed CallStack will NOT include head's call-site. This reflects the
744 standard scoping rules of implicit-parameters.
745
746 - An EvCallStack term desugars to a CoreExpr of type `IP "some str" CallStack`.
747 The desugarer will need to unwrap the IP newtype before pushing a new
748 call-site onto a given stack (See DsBinds.dsEvCallStack)
749
750 - When we emit a new wanted CallStack from rule (2) we set its origin to
751 `IPOccOrigin ip_name` instead of the original `OccurrenceOf func`
752 (see TcInteract.interactDict).
753
754 This is a bit shady, but is how we ensure that the new wanted is
755 solved like a regular IP.
756
757 -}
758
759 mkEvCast :: EvTerm -> TcCoercion -> EvTerm
760 mkEvCast ev lco
761 | ASSERT2(tcCoercionRole lco == Representational, (vcat [text "Coercion of wrong role passed to mkEvCast:", ppr ev, ppr lco]))
762 isTcReflCo lco = ev
763 | otherwise = EvCast ev lco
764
765 mkEvScSelectors :: EvTerm -> Class -> [TcType] -> [(TcPredType, EvTerm)]
766 mkEvScSelectors ev cls tys
767 = zipWith mk_pr (immSuperClasses cls tys) [0..]
768 where
769 mk_pr pred i = (pred, EvSuperClass ev i)
770
771 emptyTcEvBinds :: TcEvBinds
772 emptyTcEvBinds = EvBinds emptyBag
773
774 isEmptyTcEvBinds :: TcEvBinds -> Bool
775 isEmptyTcEvBinds (EvBinds b) = isEmptyBag b
776 isEmptyTcEvBinds (TcEvBinds {}) = panic "isEmptyTcEvBinds"
777
778
779 evTermCoercion :: EvTerm -> TcCoercion
780 -- Applied only to EvTerms of type (s~t)
781 -- See Note [Coercion evidence terms]
782 evTermCoercion (EvId v) = mkCoVarCo v
783 evTermCoercion (EvCoercion co) = co
784 evTermCoercion (EvCast tm co) = mkCoCast (evTermCoercion tm) co
785 evTermCoercion tm = pprPanic "evTermCoercion" (ppr tm)
786
787 evVarsOfTerm :: EvTerm -> VarSet
788 evVarsOfTerm (EvId v) = unitVarSet v
789 evVarsOfTerm (EvCoercion co) = coVarsOfCo co
790 evVarsOfTerm (EvDFunApp _ _ evs) = mapUnionVarSet evVarsOfTerm evs
791 evVarsOfTerm (EvSuperClass v _) = evVarsOfTerm v
792 evVarsOfTerm (EvCast tm co) = evVarsOfTerm tm `unionVarSet` coVarsOfCo co
793 evVarsOfTerm (EvDelayedError _ _) = emptyVarSet
794 evVarsOfTerm (EvLit _) = emptyVarSet
795 evVarsOfTerm (EvCallStack cs) = evVarsOfCallStack cs
796 evVarsOfTerm (EvTypeable _ ev) = evVarsOfTypeable ev
797 evVarsOfTerm (EvSelector _ _ evs) = mapUnionVarSet evVarsOfTerm evs
798
799 evVarsOfTerms :: [EvTerm] -> VarSet
800 evVarsOfTerms = mapUnionVarSet evVarsOfTerm
801
802 -- | Do SCC analysis on a bag of 'EvBind's.
803 sccEvBinds :: Bag EvBind -> [SCC EvBind]
804 sccEvBinds bs = stronglyConnCompFromEdgedVerticesUniq edges
805 where
806 edges :: [(EvBind, EvVar, [EvVar])]
807 edges = foldrBag ((:) . mk_node) [] bs
808
809 mk_node :: EvBind -> (EvBind, EvVar, [EvVar])
810 mk_node b@(EvBind { eb_lhs = var, eb_rhs = term })
811 = (b, var, nonDetEltsUFM (evVarsOfTerm term `unionVarSet`
812 coVarsOfType (varType var)))
813 -- It's OK to use nonDetEltsUFM here as stronglyConnCompFromEdgedVertices
814 -- is still deterministic even if the edges are in nondeterministic order
815 -- as explained in Note [Deterministic SCC] in Digraph.
816
817 evVarsOfCallStack :: EvCallStack -> VarSet
818 evVarsOfCallStack cs = case cs of
819 EvCsEmpty -> emptyVarSet
820 EvCsPushCall _ _ tm -> evVarsOfTerm tm
821
822 evVarsOfTypeable :: EvTypeable -> VarSet
823 evVarsOfTypeable ev =
824 case ev of
825 EvTypeableTyCon _ e -> mapUnionVarSet evVarsOfTerm e
826 EvTypeableTyApp e1 e2 -> evVarsOfTerms [e1,e2]
827 EvTypeableTrFun e1 e2 -> evVarsOfTerms [e1,e2]
828 EvTypeableTyLit e -> evVarsOfTerm e
829
830 {-
831 ************************************************************************
832 * *
833 Pretty printing
834 * *
835 ************************************************************************
836 -}
837
838 instance Outputable HsWrapper where
839 ppr co_fn = pprHsWrapper co_fn (no_parens (text "<>"))
840
841 pprHsWrapper :: HsWrapper -> (Bool -> SDoc) -> SDoc
842 -- With -fprint-typechecker-elaboration, print the wrapper
843 -- otherwise just print what's inside
844 -- The pp_thing_inside function takes Bool to say whether
845 -- it's in a position that needs parens for a non-atomic thing
846 pprHsWrapper wrap pp_thing_inside
847 = sdocWithDynFlags $ \ dflags ->
848 if gopt Opt_PrintTypecheckerElaboration dflags
849 then help pp_thing_inside wrap False
850 else pp_thing_inside False
851 where
852 help :: (Bool -> SDoc) -> HsWrapper -> Bool -> SDoc
853 -- True <=> appears in function application position
854 -- False <=> appears as body of let or lambda
855 help it WpHole = it
856 help it (WpCompose f1 f2) = help (help it f2) f1
857 help it (WpFun f1 f2 t1 _) = add_parens $ text "\\(x" <> dcolon <> ppr t1 <> text ")." <+>
858 help (\_ -> it True <+> help (\_ -> text "x") f1 True) f2 False
859 help it (WpCast co) = add_parens $ sep [it False, nest 2 (text "|>"
860 <+> pprParendCo co)]
861 help it (WpEvApp id) = no_parens $ sep [it True, nest 2 (ppr id)]
862 help it (WpTyApp ty) = no_parens $ sep [it True, text "@" <+> pprParendType ty]
863 help it (WpEvLam id) = add_parens $ sep [ text "\\" <> pp_bndr id, it False]
864 help it (WpTyLam tv) = add_parens $ sep [text "/\\" <> pp_bndr tv, it False]
865 help it (WpLet binds) = add_parens $ sep [text "let" <+> braces (ppr binds), it False]
866
867 pp_bndr v = pprBndr LambdaBind v <> dot
868
869 add_parens, no_parens :: SDoc -> Bool -> SDoc
870 add_parens d True = parens d
871 add_parens d False = d
872 no_parens d _ = d
873
874 instance Outputable TcEvBinds where
875 ppr (TcEvBinds v) = ppr v
876 ppr (EvBinds bs) = text "EvBinds" <> braces (vcat (map ppr (bagToList bs)))
877
878 instance Outputable EvBindsVar where
879 ppr (EvBindsVar { ebv_uniq = u })
880 = text "EvBindsVar" <> angleBrackets (ppr u)
881
882 instance Uniquable EvBindsVar where
883 getUnique (EvBindsVar { ebv_uniq = u }) = u
884
885 instance Outputable EvBind where
886 ppr (EvBind { eb_lhs = v, eb_rhs = e, eb_is_given = is_given })
887 = sep [ pp_gw <+> ppr v
888 , nest 2 $ equals <+> ppr e ]
889 where
890 pp_gw = brackets (if is_given then char 'G' else char 'W')
891 -- We cheat a bit and pretend EqVars are CoVars for the purposes of pretty printing
892
893 instance Outputable EvTerm where
894 ppr (EvId v) = ppr v
895 ppr (EvCast v co) = ppr v <+> (text "`cast`") <+> pprParendCo co
896 ppr (EvCoercion co) = text "CO" <+> ppr co
897 ppr (EvSuperClass d n) = text "sc" <> parens (ppr (d,n))
898 ppr (EvDFunApp df tys ts) = ppr df <+> sep [ char '@' <> ppr tys, ppr ts ]
899 ppr (EvLit l) = ppr l
900 ppr (EvCallStack cs) = ppr cs
901 ppr (EvDelayedError ty msg) = text "error"
902 <+> sep [ char '@' <> ppr ty, ppr msg ]
903 ppr (EvTypeable ty ev) = ppr ev <+> dcolon <+> text "Typeable" <+> ppr ty
904 ppr (EvSelector sel tys ts) = ppr sel <+> sep [ char '@' <> ppr tys, ppr ts]
905
906 instance Outputable EvLit where
907 ppr (EvNum n) = integer n
908 ppr (EvStr s) = text (show s)
909
910 instance Outputable EvCallStack where
911 ppr EvCsEmpty
912 = text "[]"
913 ppr (EvCsPushCall name loc tm)
914 = ppr (name,loc) <+> text ":" <+> ppr tm
915
916 instance Outputable EvTypeable where
917 ppr (EvTypeableTyCon ts _) = text "TyCon" <+> ppr ts
918 ppr (EvTypeableTyApp t1 t2) = parens (ppr t1 <+> ppr t2)
919 ppr (EvTypeableTrFun t1 t2) = parens (ppr t1 <+> arrow <+> ppr t2)
920 ppr (EvTypeableTyLit t1) = text "TyLit" <> ppr t1
921
922
923 ----------------------------------------------------------------------
924 -- Helper functions for dealing with IP newtype-dictionaries
925 ----------------------------------------------------------------------
926
927 -- | Create a 'Coercion' that unwraps an implicit-parameter or
928 -- overloaded-label dictionary to expose the underlying value. We
929 -- expect the 'Type' to have the form `IP sym ty` or `IsLabel sym ty`,
930 -- and return a 'Coercion' `co :: IP sym ty ~ ty` or
931 -- `co :: IsLabel sym ty ~ Proxy# sym -> ty`. See also
932 -- Note [Type-checking overloaded labels] in TcExpr.
933 unwrapIP :: Type -> CoercionR
934 unwrapIP ty =
935 case unwrapNewTyCon_maybe tc of
936 Just (_,_,ax) -> mkUnbranchedAxInstCo Representational ax tys []
937 Nothing -> pprPanic "unwrapIP" $
938 text "The dictionary for" <+> quotes (ppr tc)
939 <+> text "is not a newtype!"
940 where
941 (tc, tys) = splitTyConApp ty
942
943 -- | Create a 'Coercion' that wraps a value in an implicit-parameter
944 -- dictionary. See 'unwrapIP'.
945 wrapIP :: Type -> CoercionR
946 wrapIP ty = mkSymCo (unwrapIP ty)