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