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