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