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