Documentation for (&&) and (&&) states that they are lazy in their second argument...
[ghc.git] / compiler / typecheck / ClsInst.hs
1 {-# LANGUAGE CPP #-}
2
3 module ClsInst (
4 matchGlobalInst,
5 ClsInstResult(..),
6 InstanceWhat(..), safeOverlap, instanceReturnsDictCon,
7 AssocInstInfo(..), isNotAssociated
8 ) where
9
10 #include "HsVersions.h"
11
12 import GhcPrelude
13
14 import TcEnv
15 import TcRnMonad
16 import TcType
17 import TcTypeable
18 import TcMType
19 import TcEvidence
20 import Predicate
21 import RnEnv( addUsedGRE )
22 import RdrName( lookupGRE_FieldLabel )
23 import InstEnv
24 import Inst( instDFunType )
25 import FamInst( tcGetFamInstEnvs, tcInstNewTyCon_maybe, tcLookupDataFamInst )
26
27 import TysWiredIn
28 import TysPrim( eqPrimTyCon, eqReprPrimTyCon )
29 import PrelNames
30
31 import Id
32 import Type
33 import MkCore ( mkStringExprFS, mkNaturalExpr )
34
35 import Name ( Name, pprDefinedAt )
36 import VarEnv ( VarEnv )
37 import DataCon
38 import TyCon
39 import Class
40 import DynFlags
41 import Outputable
42 import Util( splitAtList, fstOf3 )
43 import Data.Maybe
44
45 {- *******************************************************************
46 * *
47 A helper for associated types within
48 class instance declarations
49 * *
50 **********************************************************************-}
51
52 -- | Extra information about the parent instance declaration, needed
53 -- when type-checking associated types. The 'Class' is the enclosing
54 -- class, the [TyVar] are the /scoped/ type variable of the instance decl.
55 -- The @VarEnv Type@ maps class variables to their instance types.
56 data AssocInstInfo
57 = NotAssociated
58 | InClsInst { ai_class :: Class
59 , ai_tyvars :: [TyVar] -- ^ The /scoped/ tyvars of the instance
60 -- Why scoped? See bind_me in
61 -- TcValidity.checkConsistentFamInst
62 , ai_inst_env :: VarEnv Type -- ^ Maps /class/ tyvars to their instance types
63 -- See Note [Matching in the consistent-instantation check]
64 }
65
66 isNotAssociated :: AssocInstInfo -> Bool
67 isNotAssociated NotAssociated = True
68 isNotAssociated (InClsInst {}) = False
69
70
71 {- *******************************************************************
72 * *
73 Class lookup
74 * *
75 **********************************************************************-}
76
77 -- | Indicates if Instance met the Safe Haskell overlapping instances safety
78 -- check.
79 --
80 -- See Note [Safe Haskell Overlapping Instances] in TcSimplify
81 -- See Note [Safe Haskell Overlapping Instances Implementation] in TcSimplify
82 type SafeOverlapping = Bool
83
84 data ClsInstResult
85 = NoInstance -- Definitely no instance
86
87 | OneInst { cir_new_theta :: [TcPredType]
88 , cir_mk_ev :: [EvExpr] -> EvTerm
89 , cir_what :: InstanceWhat }
90
91 | NotSure -- Multiple matches and/or one or more unifiers
92
93 data InstanceWhat
94 = BuiltinInstance
95 | BuiltinEqInstance -- A built-in "equality instance"; see the
96 -- TcSMonad Note [Solved dictionaries]
97 | LocalInstance
98 | TopLevInstance { iw_dfun_id :: DFunId
99 , iw_safe_over :: SafeOverlapping }
100
101 instance Outputable ClsInstResult where
102 ppr NoInstance = text "NoInstance"
103 ppr NotSure = text "NotSure"
104 ppr (OneInst { cir_new_theta = ev
105 , cir_what = what })
106 = text "OneInst" <+> vcat [ppr ev, ppr what]
107
108 instance Outputable InstanceWhat where
109 ppr BuiltinInstance = text "a built-in instance"
110 ppr BuiltinEqInstance = text "a built-in equality instance"
111 ppr LocalInstance = text "a locally-quantified instance"
112 ppr (TopLevInstance { iw_dfun_id = dfun })
113 = hang (text "instance" <+> pprSigmaType (idType dfun))
114 2 (text "--" <+> pprDefinedAt (idName dfun))
115
116 safeOverlap :: InstanceWhat -> Bool
117 safeOverlap (TopLevInstance { iw_safe_over = so }) = so
118 safeOverlap _ = True
119
120 instanceReturnsDictCon :: InstanceWhat -> Bool
121 -- See Note [Solved dictionaries] in TcSMonad
122 instanceReturnsDictCon (TopLevInstance {}) = True
123 instanceReturnsDictCon BuiltinInstance = True
124 instanceReturnsDictCon BuiltinEqInstance = False
125 instanceReturnsDictCon LocalInstance = False
126
127 matchGlobalInst :: DynFlags
128 -> Bool -- True <=> caller is the short-cut solver
129 -- See Note [Shortcut solving: overlap]
130 -> Class -> [Type] -> TcM ClsInstResult
131 matchGlobalInst dflags short_cut clas tys
132 | cls_name == knownNatClassName
133 = matchKnownNat dflags short_cut clas tys
134 | cls_name == knownSymbolClassName
135 = matchKnownSymbol dflags short_cut clas tys
136 | isCTupleClass clas = matchCTuple clas tys
137 | cls_name == typeableClassName = matchTypeable clas tys
138 | clas `hasKey` heqTyConKey = matchHeteroEquality tys
139 | clas `hasKey` eqTyConKey = matchHomoEquality tys
140 | clas `hasKey` coercibleTyConKey = matchCoercible tys
141 | cls_name == hasFieldClassName = matchHasField dflags short_cut clas tys
142 | otherwise = matchInstEnv dflags short_cut clas tys
143 where
144 cls_name = className clas
145
146
147 {- ********************************************************************
148 * *
149 Looking in the instance environment
150 * *
151 ***********************************************************************-}
152
153
154 matchInstEnv :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
155 matchInstEnv dflags short_cut_solver clas tys
156 = do { instEnvs <- tcGetInstEnvs
157 ; let safeOverlapCheck = safeHaskell dflags `elem` [Sf_Safe, Sf_Trustworthy]
158 (matches, unify, unsafeOverlaps) = lookupInstEnv True instEnvs clas tys
159 safeHaskFail = safeOverlapCheck && not (null unsafeOverlaps)
160 ; traceTc "matchInstEnv" $
161 vcat [ text "goal:" <+> ppr clas <+> ppr tys
162 , text "matches:" <+> ppr matches
163 , text "unify:" <+> ppr unify ]
164 ; case (matches, unify, safeHaskFail) of
165
166 -- Nothing matches
167 ([], [], _)
168 -> do { traceTc "matchClass not matching" (ppr pred)
169 ; return NoInstance }
170
171 -- A single match (& no safe haskell failure)
172 ([(ispec, inst_tys)], [], False)
173 | short_cut_solver -- Called from the short-cut solver
174 , isOverlappable ispec
175 -- If the instance has OVERLAPPABLE or OVERLAPS or INCOHERENT
176 -- then don't let the short-cut solver choose it, because a
177 -- later instance might overlap it. #14434 is an example
178 -- See Note [Shortcut solving: overlap]
179 -> do { traceTc "matchClass: ignoring overlappable" (ppr pred)
180 ; return NotSure }
181
182 | otherwise
183 -> do { let dfun_id = instanceDFunId ispec
184 ; traceTc "matchClass success" $
185 vcat [text "dict" <+> ppr pred,
186 text "witness" <+> ppr dfun_id
187 <+> ppr (idType dfun_id) ]
188 -- Record that this dfun is needed
189 ; match_one (null unsafeOverlaps) dfun_id inst_tys }
190
191 -- More than one matches (or Safe Haskell fail!). Defer any
192 -- reactions of a multitude until we learn more about the reagent
193 _ -> do { traceTc "matchClass multiple matches, deferring choice" $
194 vcat [text "dict" <+> ppr pred,
195 text "matches" <+> ppr matches]
196 ; return NotSure } }
197 where
198 pred = mkClassPred clas tys
199
200 match_one :: SafeOverlapping -> DFunId -> [DFunInstType] -> TcM ClsInstResult
201 -- See Note [DFunInstType: instantiating types] in InstEnv
202 match_one so dfun_id mb_inst_tys
203 = do { traceTc "match_one" (ppr dfun_id $$ ppr mb_inst_tys)
204 ; (tys, theta) <- instDFunType dfun_id mb_inst_tys
205 ; traceTc "match_one 2" (ppr dfun_id $$ ppr tys $$ ppr theta)
206 ; return $ OneInst { cir_new_theta = theta
207 , cir_mk_ev = evDFunApp dfun_id tys
208 , cir_what = TopLevInstance { iw_dfun_id = dfun_id
209 , iw_safe_over = so } } }
210
211
212 {- Note [Shortcut solving: overlap]
213 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
214 Suppose we have
215 instance {-# OVERLAPPABLE #-} C a where ...
216 and we are typechecking
217 f :: C a => a -> a
218 f = e -- Gives rise to [W] C a
219
220 We don't want to solve the wanted constraint with the overlappable
221 instance; rather we want to use the supplied (C a)! That was the whole
222 point of it being overlappable! #14434 wwas an example.
223
224 Alas even if the instance has no overlap flag, thus
225 instance C a where ...
226 there is nothing to stop it being overlapped. GHC provides no way to
227 declare an instance as "final" so it can't be overlapped. But really
228 only final instances are OK for short-cut solving. Sigh. #15135
229 was a puzzling example.
230 -}
231
232
233 {- ********************************************************************
234 * *
235 Class lookup for CTuples
236 * *
237 ***********************************************************************-}
238
239 matchCTuple :: Class -> [Type] -> TcM ClsInstResult
240 matchCTuple clas tys -- (isCTupleClass clas) holds
241 = return (OneInst { cir_new_theta = tys
242 , cir_mk_ev = tuple_ev
243 , cir_what = BuiltinInstance })
244 -- The dfun *is* the data constructor!
245 where
246 data_con = tyConSingleDataCon (classTyCon clas)
247 tuple_ev = evDFunApp (dataConWrapId data_con) tys
248
249 {- ********************************************************************
250 * *
251 Class lookup for Literals
252 * *
253 ***********************************************************************-}
254
255 {-
256 Note [KnownNat & KnownSymbol and EvLit]
257 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
258 A part of the type-level literals implementation are the classes
259 "KnownNat" and "KnownSymbol", which provide a "smart" constructor for
260 defining singleton values. Here is the key stuff from GHC.TypeLits
261
262 class KnownNat (n :: Nat) where
263 natSing :: SNat n
264
265 newtype SNat (n :: Nat) = SNat Integer
266
267 Conceptually, this class has infinitely many instances:
268
269 instance KnownNat 0 where natSing = SNat 0
270 instance KnownNat 1 where natSing = SNat 1
271 instance KnownNat 2 where natSing = SNat 2
272 ...
273
274 In practice, we solve `KnownNat` predicates in the type-checker
275 (see typecheck/TcInteract.hs) because we can't have infinitely many instances.
276 The evidence (aka "dictionary") for `KnownNat` is of the form `EvLit (EvNum n)`.
277
278 We make the following assumptions about dictionaries in GHC:
279 1. The "dictionary" for classes with a single method---like `KnownNat`---is
280 a newtype for the type of the method, so using a evidence amounts
281 to a coercion, and
282 2. Newtypes use the same representation as their definition types.
283
284 So, the evidence for `KnownNat` is just a value of the representation type,
285 wrapped in two newtype constructors: one to make it into a `SNat` value,
286 and another to make it into a `KnownNat` dictionary.
287
288 Also note that `natSing` and `SNat` are never actually exposed from the
289 library---they are just an implementation detail. Instead, users see
290 a more convenient function, defined in terms of `natSing`:
291
292 natVal :: KnownNat n => proxy n -> Integer
293
294 The reason we don't use this directly in the class is that it is simpler
295 and more efficient to pass around an integer rather than an entire function,
296 especially when the `KnowNat` evidence is packaged up in an existential.
297
298 The story for kind `Symbol` is analogous:
299 * class KnownSymbol
300 * newtype SSymbol
301 * Evidence: a Core literal (e.g. mkNaturalExpr)
302
303
304 Note [Fabricating Evidence for Literals in Backpack]
305 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
306
307 Let `T` be a type of kind `Nat`. When solving for a purported instance
308 of `KnownNat T`, ghc tries to resolve the type `T` to an integer `n`,
309 in which case the evidence `EvLit (EvNum n)` is generated on the
310 fly. It might appear that this is sufficient as users cannot define
311 their own instances of `KnownNat`. However, for backpack module this
312 would not work (see issue #15379). Consider the signature `Abstract`
313
314 > signature Abstract where
315 > data T :: Nat
316 > instance KnownNat T
317
318 and a module `Util` that depends on it:
319
320 > module Util where
321 > import Abstract
322 > printT :: IO ()
323 > printT = do print $ natVal (Proxy :: Proxy T)
324
325 Clearly, we need to "use" the dictionary associated with `KnownNat T`
326 in the module `Util`, but it is too early for the compiler to produce
327 a real dictionary as we still have not fixed what `T` is. Only when we
328 mixin a concrete module
329
330 > module Concrete where
331 > type T = 42
332
333 do we really get hold of the underlying integer. So the strategy that
334 we follow is the following
335
336 1. If T is indeed available as a type alias for an integer constant,
337 generate the dictionary on the fly, failing which
338
339 2. Look up the type class environment for the evidence.
340
341 Finally actual code gets generate for Util only when a module like
342 Concrete gets "mixed-in" in place of the signature Abstract. As a
343 result all things, including the typeclass instances, in Concrete gets
344 reexported. So `KnownNat` gets resolved the normal way post-Backpack.
345
346 A similar generation works for `KnownSymbol` as well
347
348 -}
349
350 matchKnownNat :: DynFlags
351 -> Bool -- True <=> caller is the short-cut solver
352 -- See Note [Shortcut solving: overlap]
353 -> Class -> [Type] -> TcM ClsInstResult
354 matchKnownNat _ _ clas [ty] -- clas = KnownNat
355 | Just n <- isNumLitTy ty = do
356 et <- mkNaturalExpr n
357 makeLitDict clas ty et
358 matchKnownNat df sc clas tys = matchInstEnv df sc clas tys
359 -- See Note [Fabricating Evidence for Literals in Backpack] for why
360 -- this lookup into the instance environment is required.
361
362 matchKnownSymbol :: DynFlags
363 -> Bool -- True <=> caller is the short-cut solver
364 -- See Note [Shortcut solving: overlap]
365 -> Class -> [Type] -> TcM ClsInstResult
366 matchKnownSymbol _ _ clas [ty] -- clas = KnownSymbol
367 | Just s <- isStrLitTy ty = do
368 et <- mkStringExprFS s
369 makeLitDict clas ty et
370 matchKnownSymbol df sc clas tys = matchInstEnv df sc clas tys
371 -- See Note [Fabricating Evidence for Literals in Backpack] for why
372 -- this lookup into the instance environment is required.
373
374 makeLitDict :: Class -> Type -> EvExpr -> TcM ClsInstResult
375 -- makeLitDict adds a coercion that will convert the literal into a dictionary
376 -- of the appropriate type. See Note [KnownNat & KnownSymbol and EvLit]
377 -- in TcEvidence. The coercion happens in 2 steps:
378 --
379 -- Integer -> SNat n -- representation of literal to singleton
380 -- SNat n -> KnownNat n -- singleton to dictionary
381 --
382 -- The process is mirrored for Symbols:
383 -- String -> SSymbol n
384 -- SSymbol n -> KnownSymbol n
385 makeLitDict clas ty et
386 | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]
387 -- co_dict :: KnownNat n ~ SNat n
388 , [ meth ] <- classMethods clas
389 , Just tcRep <- tyConAppTyCon_maybe -- SNat
390 $ funResultTy -- SNat n
391 $ dropForAlls -- KnownNat n => SNat n
392 $ idType meth -- forall n. KnownNat n => SNat n
393 , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]
394 -- SNat n ~ Integer
395 , let ev_tm = mkEvCast et (mkTcSymCo (mkTcTransCo co_dict co_rep))
396 = return $ OneInst { cir_new_theta = []
397 , cir_mk_ev = \_ -> ev_tm
398 , cir_what = BuiltinInstance }
399
400 | otherwise
401 = pprPanic "makeLitDict" $
402 text "Unexpected evidence for" <+> ppr (className clas)
403 $$ vcat (map (ppr . idType) (classMethods clas))
404
405 {- ********************************************************************
406 * *
407 Class lookup for Typeable
408 * *
409 ***********************************************************************-}
410
411 -- | Assumes that we've checked that this is the 'Typeable' class,
412 -- and it was applied to the correct argument.
413 matchTypeable :: Class -> [Type] -> TcM ClsInstResult
414 matchTypeable clas [k,t] -- clas = Typeable
415 -- For the first two cases, See Note [No Typeable for polytypes or qualified types]
416 | isForAllTy k = return NoInstance -- Polytype
417 | isJust (tcSplitPredFunTy_maybe t) = return NoInstance -- Qualified type
418
419 -- Now cases that do work
420 | k `eqType` typeNatKind = doTyLit knownNatClassName t
421 | k `eqType` typeSymbolKind = doTyLit knownSymbolClassName t
422 | tcIsConstraintKind t = doTyConApp clas t constraintKindTyCon []
423 | Just (arg,ret) <- splitFunTy_maybe t = doFunTy clas t arg ret
424 | Just (tc, ks) <- splitTyConApp_maybe t -- See Note [Typeable (T a b c)]
425 , onlyNamedBndrsApplied tc ks = doTyConApp clas t tc ks
426 | Just (f,kt) <- splitAppTy_maybe t = doTyApp clas t f kt
427
428 matchTypeable _ _ = return NoInstance
429
430 -- | Representation for a type @ty@ of the form @arg -> ret@.
431 doFunTy :: Class -> Type -> Type -> Type -> TcM ClsInstResult
432 doFunTy clas ty arg_ty ret_ty
433 = return $ OneInst { cir_new_theta = preds
434 , cir_mk_ev = mk_ev
435 , cir_what = BuiltinInstance }
436 where
437 preds = map (mk_typeable_pred clas) [arg_ty, ret_ty]
438 mk_ev [arg_ev, ret_ev] = evTypeable ty $
439 EvTypeableTrFun (EvExpr arg_ev) (EvExpr ret_ev)
440 mk_ev _ = panic "TcInteract.doFunTy"
441
442
443 -- | Representation for type constructor applied to some kinds.
444 -- 'onlyNamedBndrsApplied' has ensured that this application results in a type
445 -- of monomorphic kind (e.g. all kind variables have been instantiated).
446 doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcM ClsInstResult
447 doTyConApp clas ty tc kind_args
448 | tyConIsTypeable tc
449 = return $ OneInst { cir_new_theta = (map (mk_typeable_pred clas) kind_args)
450 , cir_mk_ev = mk_ev
451 , cir_what = BuiltinInstance }
452 | otherwise
453 = return NoInstance
454 where
455 mk_ev kinds = evTypeable ty $ EvTypeableTyCon tc (map EvExpr kinds)
456
457 -- | Representation for TyCon applications of a concrete kind. We just use the
458 -- kind itself, but first we must make sure that we've instantiated all kind-
459 -- polymorphism, but no more.
460 onlyNamedBndrsApplied :: TyCon -> [KindOrType] -> Bool
461 onlyNamedBndrsApplied tc ks
462 = all isNamedTyConBinder used_bndrs &&
463 not (any isNamedTyConBinder leftover_bndrs)
464 where
465 bndrs = tyConBinders tc
466 (used_bndrs, leftover_bndrs) = splitAtList ks bndrs
467
468 doTyApp :: Class -> Type -> Type -> KindOrType -> TcM ClsInstResult
469 -- Representation for an application of a type to a type-or-kind.
470 -- This may happen when the type expression starts with a type variable.
471 -- Example (ignoring kind parameter):
472 -- Typeable (f Int Char) -->
473 -- (Typeable (f Int), Typeable Char) -->
474 -- (Typeable f, Typeable Int, Typeable Char) --> (after some simp. steps)
475 -- Typeable f
476 doTyApp clas ty f tk
477 | isForAllTy (tcTypeKind f)
478 = return NoInstance -- We can't solve until we know the ctr.
479 | otherwise
480 = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) [f, tk]
481 , cir_mk_ev = mk_ev
482 , cir_what = BuiltinInstance }
483 where
484 mk_ev [t1,t2] = evTypeable ty $ EvTypeableTyApp (EvExpr t1) (EvExpr t2)
485 mk_ev _ = panic "doTyApp"
486
487
488 -- Emit a `Typeable` constraint for the given type.
489 mk_typeable_pred :: Class -> Type -> PredType
490 mk_typeable_pred clas ty = mkClassPred clas [ tcTypeKind ty, ty ]
491
492 -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
493 -- we generate a sub-goal for the appropriate class.
494 -- See Note [Typeable for Nat and Symbol]
495 doTyLit :: Name -> Type -> TcM ClsInstResult
496 doTyLit kc t = do { kc_clas <- tcLookupClass kc
497 ; let kc_pred = mkClassPred kc_clas [ t ]
498 mk_ev [ev] = evTypeable t $ EvTypeableTyLit (EvExpr ev)
499 mk_ev _ = panic "doTyLit"
500 ; return (OneInst { cir_new_theta = [kc_pred]
501 , cir_mk_ev = mk_ev
502 , cir_what = BuiltinInstance }) }
503
504 {- Note [Typeable (T a b c)]
505 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
506 For type applications we always decompose using binary application,
507 via doTyApp, until we get to a *kind* instantiation. Example
508 Proxy :: forall k. k -> *
509
510 To solve Typeable (Proxy (* -> *) Maybe) we
511 - First decompose with doTyApp,
512 to get (Typeable (Proxy (* -> *))) and Typeable Maybe
513 - Then solve (Typeable (Proxy (* -> *))) with doTyConApp
514
515 If we attempt to short-cut by solving it all at once, via
516 doTyConApp
517
518 (this note is sadly truncated FIXME)
519
520
521 Note [No Typeable for polytypes or qualified types]
522 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
523 We do not support impredicative typeable, such as
524 Typeable (forall a. a->a)
525 Typeable (Eq a => a -> a)
526 Typeable (() => Int)
527 Typeable (((),()) => Int)
528
529 See #9858. For forall's the case is clear: we simply don't have
530 a TypeRep for them. For qualified but not polymorphic types, like
531 (Eq a => a -> a), things are murkier. But:
532
533 * We don't need a TypeRep for these things. TypeReps are for
534 monotypes only.
535
536 * Perhaps we could treat `=>` as another type constructor for `Typeable`
537 purposes, and thus support things like `Eq Int => Int`, however,
538 at the current state of affairs this would be an odd exception as
539 no other class works with impredicative types.
540 For now we leave it off, until we have a better story for impredicativity.
541
542
543 Note [Typeable for Nat and Symbol]
544 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
545 We have special Typeable instances for Nat and Symbol. Roughly we
546 have this instance, implemented here by doTyLit:
547 instance KnownNat n => Typeable (n :: Nat) where
548 typeRep = typeNatTypeRep @n
549 where
550 Data.Typeable.Internals.typeNatTypeRep :: KnownNat a => TypeRep a
551
552 Ultimately typeNatTypeRep uses 'natSing' from KnownNat to get a
553 runtime value 'n'; it turns it into a string with 'show' and uses
554 that to whiz up a TypeRep TyCon for 'n', with mkTypeLitTyCon.
555 See #10348.
556
557 Because of this rule it's inadvisable (see #15322) to have a constraint
558 f :: (Typeable (n :: Nat)) => blah
559 in a function signature; it gives rise to overlap problems just as
560 if you'd written
561 f :: Eq [a] => blah
562 -}
563
564 {- ********************************************************************
565 * *
566 Class lookup for lifted equality
567 * *
568 ***********************************************************************-}
569
570 -- See also Note [The equality types story] in TysPrim
571 matchHeteroEquality :: [Type] -> TcM ClsInstResult
572 -- Solves (t1 ~~ t2)
573 matchHeteroEquality args
574 = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon args ]
575 , cir_mk_ev = evDataConApp heqDataCon args
576 , cir_what = BuiltinEqInstance })
577
578 matchHomoEquality :: [Type] -> TcM ClsInstResult
579 -- Solves (t1 ~ t2)
580 matchHomoEquality args@[k,t1,t2]
581 = return (OneInst { cir_new_theta = [ mkTyConApp eqPrimTyCon [k,k,t1,t2] ]
582 , cir_mk_ev = evDataConApp eqDataCon args
583 , cir_what = BuiltinEqInstance })
584 matchHomoEquality args = pprPanic "matchHomoEquality" (ppr args)
585
586 -- See also Note [The equality types story] in TysPrim
587 matchCoercible :: [Type] -> TcM ClsInstResult
588 matchCoercible args@[k, t1, t2]
589 = return (OneInst { cir_new_theta = [ mkTyConApp eqReprPrimTyCon args' ]
590 , cir_mk_ev = evDataConApp coercibleDataCon args
591 , cir_what = BuiltinEqInstance })
592 where
593 args' = [k, k, t1, t2]
594 matchCoercible args = pprPanic "matchLiftedCoercible" (ppr args)
595
596
597 {- ********************************************************************
598 * *
599 Class lookup for overloaded record fields
600 * *
601 ***********************************************************************-}
602
603 {-
604 Note [HasField instances]
605 ~~~~~~~~~~~~~~~~~~~~~~~~~
606 Suppose we have
607
608 data T y = MkT { foo :: [y] }
609
610 and `foo` is in scope. Then GHC will automatically solve a constraint like
611
612 HasField "foo" (T Int) b
613
614 by emitting a new wanted
615
616 T alpha -> [alpha] ~# T Int -> b
617
618 and building a HasField dictionary out of the selector function `foo`,
619 appropriately cast.
620
621 The HasField class is defined (in GHC.Records) thus:
622
623 class HasField (x :: k) r a | x r -> a where
624 getField :: r -> a
625
626 Since this is a one-method class, it is represented as a newtype.
627 Hence we can solve `HasField "foo" (T Int) b` by taking an expression
628 of type `T Int -> b` and casting it using the newtype coercion.
629 Note that
630
631 foo :: forall y . T y -> [y]
632
633 so the expression we construct is
634
635 foo @alpha |> co
636
637 where
638
639 co :: (T alpha -> [alpha]) ~# HasField "foo" (T Int) b
640
641 is built from
642
643 co1 :: (T alpha -> [alpha]) ~# (T Int -> b)
644
645 which is the new wanted, and
646
647 co2 :: (T Int -> b) ~# HasField "foo" (T Int) b
648
649 which can be derived from the newtype coercion.
650
651 If `foo` is not in scope, or has a higher-rank or existentially
652 quantified type, then the constraint is not solved automatically, but
653 may be solved by a user-supplied HasField instance. Similarly, if we
654 encounter a HasField constraint where the field is not a literal
655 string, or does not belong to the type, then we fall back on the
656 normal constraint solver behaviour.
657 -}
658
659 -- See Note [HasField instances]
660 matchHasField :: DynFlags -> Bool -> Class -> [Type] -> TcM ClsInstResult
661 matchHasField dflags short_cut clas tys
662 = do { fam_inst_envs <- tcGetFamInstEnvs
663 ; rdr_env <- getGlobalRdrEnv
664 ; case tys of
665 -- We are matching HasField {k} x r a...
666 [_k_ty, x_ty, r_ty, a_ty]
667 -- x should be a literal string
668 | Just x <- isStrLitTy x_ty
669 -- r should be an applied type constructor
670 , Just (tc, args) <- tcSplitTyConApp_maybe r_ty
671 -- use representation tycon (if data family); it has the fields
672 , let r_tc = fstOf3 (tcLookupDataFamInst fam_inst_envs tc args)
673 -- x should be a field of r
674 , Just fl <- lookupTyConFieldLabel x r_tc
675 -- the field selector should be in scope
676 , Just gre <- lookupGRE_FieldLabel rdr_env fl
677
678 -> do { sel_id <- tcLookupId (flSelector fl)
679 ; (tv_prs, preds, sel_ty) <- tcInstType newMetaTyVars sel_id
680
681 -- The first new wanted constraint equates the actual
682 -- type of the selector with the type (r -> a) within
683 -- the HasField x r a dictionary. The preds will
684 -- typically be empty, but if the datatype has a
685 -- "stupid theta" then we have to include it here.
686 ; let theta = mkPrimEqPred sel_ty (mkVisFunTy r_ty a_ty) : preds
687
688 -- Use the equality proof to cast the selector Id to
689 -- type (r -> a), then use the newtype coercion to cast
690 -- it to a HasField dictionary.
691 mk_ev (ev1:evs) = evSelector sel_id tvs evs `evCast` co
692 where
693 co = mkTcSubCo (evTermCoercion (EvExpr ev1))
694 `mkTcTransCo` mkTcSymCo co2
695 mk_ev [] = panic "matchHasField.mk_ev"
696
697 Just (_, co2) = tcInstNewTyCon_maybe (classTyCon clas)
698 tys
699
700 tvs = mkTyVarTys (map snd tv_prs)
701
702 -- The selector must not be "naughty" (i.e. the field
703 -- cannot have an existentially quantified type), and
704 -- it must not be higher-rank.
705 ; if not (isNaughtyRecordSelector sel_id) && isTauTy sel_ty
706 then do { addUsedGRE True gre
707 ; return OneInst { cir_new_theta = theta
708 , cir_mk_ev = mk_ev
709 , cir_what = BuiltinInstance } }
710 else matchInstEnv dflags short_cut clas tys }
711
712 _ -> matchInstEnv dflags short_cut clas tys }