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