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