284d6a95d3d915fd4e68f3684c9878eac34084cd
[ghc.git] / compiler / typecheck / Inst.hs
1 {-
2 (c) The University of Glasgow 2006
3 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
4
5
6 The @Inst@ type: dictionaries or method instances
7 -}
8
9 {-# LANGUAGE CPP, MultiWayIf, TupleSections #-}
10 {-# LANGUAGE FlexibleContexts #-}
11
12 module Inst (
13 deeplySkolemise,
14 topInstantiate, topInstantiateInferred, deeplyInstantiate,
15 instCall, instDFunType, instStupidTheta, instTyVarsWith,
16 newWanted, newWanteds,
17
18 tcInstTyBinders, tcInstTyBinder,
19
20 newOverloadedLit, mkOverLit,
21
22 newClsInst,
23 tcGetInsts, tcGetInstEnvs, getOverlapFlag,
24 tcExtendLocalInstEnv,
25 instCallConstraints, newMethodFromName,
26 tcSyntaxName,
27
28 -- Simple functions over evidence variables
29 tyCoVarsOfWC,
30 tyCoVarsOfCt, tyCoVarsOfCts,
31 ) where
32
33 #include "HsVersions.h"
34
35 import GhcPrelude
36
37 import {-# SOURCE #-} TcExpr( tcPolyExpr, tcSyntaxOp )
38 import {-# SOURCE #-} TcUnify( unifyType, unifyKind )
39
40 import BasicTypes ( IntegralLit(..), SourceText(..) )
41 import FastString
42 import HsSyn
43 import TcHsSyn
44 import TcRnMonad
45 import TcEnv
46 import TcEvidence
47 import InstEnv
48 import TysWiredIn ( heqDataCon, eqDataCon )
49 import CoreSyn ( isOrphan )
50 import FunDeps
51 import TcMType
52 import Type
53 import TyCoRep
54 import TcType
55 import HscTypes
56 import Class( Class )
57 import MkId( mkDictFunId )
58 import CoreSyn( Expr(..) ) -- For the Coercion constructor
59 import Id
60 import Name
61 import Var ( EvVar, mkTyVar, tyVarName, VarBndr(..) )
62 import DataCon
63 import VarEnv
64 import PrelNames
65 import SrcLoc
66 import DynFlags
67 import Util
68 import Outputable
69 import qualified GHC.LanguageExtensions as LangExt
70
71 import Control.Monad( unless )
72
73 {-
74 ************************************************************************
75 * *
76 Creating and emittind constraints
77 * *
78 ************************************************************************
79 -}
80
81 newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr GhcTcId)
82 -- Used when Name is the wired-in name for a wired-in class method,
83 -- so the caller knows its type for sure, which should be of form
84 -- forall a. C a => <blah>
85 -- newMethodFromName is supposed to instantiate just the outer
86 -- type variable and constraint
87
88 newMethodFromName origin name inst_ty
89 = do { id <- tcLookupId name
90 -- Use tcLookupId not tcLookupGlobalId; the method is almost
91 -- always a class op, but with -XRebindableSyntax GHC is
92 -- meant to find whatever thing is in scope, and that may
93 -- be an ordinary function.
94
95 ; let ty = piResultTy (idType id) inst_ty
96 (theta, _caller_knows_this) = tcSplitPhiTy ty
97 ; wrap <- ASSERT( not (isForAllTy ty) && isSingleton theta )
98 instCall origin [inst_ty] theta
99
100 ; return (mkHsWrap wrap (HsVar noExt (noLoc id))) }
101
102 {-
103 ************************************************************************
104 * *
105 Deep instantiation and skolemisation
106 * *
107 ************************************************************************
108
109 Note [Deep skolemisation]
110 ~~~~~~~~~~~~~~~~~~~~~~~~~
111 deeplySkolemise decomposes and skolemises a type, returning a type
112 with all its arrows visible (ie not buried under foralls)
113
114 Examples:
115
116 deeplySkolemise (Int -> forall a. Ord a => blah)
117 = ( wp, [a], [d:Ord a], Int -> blah )
118 where wp = \x:Int. /\a. \(d:Ord a). <hole> x
119
120 deeplySkolemise (forall a. Ord a => Maybe a -> forall b. Eq b => blah)
121 = ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah )
122 where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x
123
124 In general,
125 if deeplySkolemise ty = (wrap, tvs, evs, rho)
126 and e :: rho
127 then wrap e :: ty
128 and 'wrap' binds tvs, evs
129
130 ToDo: this eta-abstraction plays fast and loose with termination,
131 because it can introduce extra lambdas. Maybe add a `seq` to
132 fix this
133 -}
134
135 deeplySkolemise :: TcSigmaType
136 -> TcM ( HsWrapper
137 , [(Name,TyVar)] -- All skolemised variables
138 , [EvVar] -- All "given"s
139 , TcRhoType )
140
141 deeplySkolemise ty
142 = go init_subst ty
143 where
144 init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
145
146 go subst ty
147 | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
148 = do { let arg_tys' = substTys subst arg_tys
149 ; ids1 <- newSysLocalIds (fsLit "dk") arg_tys'
150 ; (subst', tvs1) <- tcInstSkolTyVarsX subst tvs
151 ; ev_vars1 <- newEvVars (substTheta subst' theta)
152 ; (wrap, tvs_prs2, ev_vars2, rho) <- go subst' ty'
153 ; let tv_prs1 = map tyVarName tvs `zip` tvs1
154 ; return ( mkWpLams ids1
155 <.> mkWpTyLams tvs1
156 <.> mkWpLams ev_vars1
157 <.> wrap
158 <.> mkWpEvVarApps ids1
159 , tv_prs1 ++ tvs_prs2
160 , ev_vars1 ++ ev_vars2
161 , mkFunTys arg_tys' rho ) }
162
163 | otherwise
164 = return (idHsWrapper, [], [], substTy subst ty)
165 -- substTy is a quick no-op on an empty substitution
166
167 -- | Instantiate all outer type variables
168 -- and any context. Never looks through arrows.
169 topInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
170 -- if topInstantiate ty = (wrap, rho)
171 -- and e :: ty
172 -- then wrap e :: rho (that is, wrap :: ty "->" rho)
173 topInstantiate = top_instantiate True
174
175 -- | Instantiate all outer 'Inferred' binders
176 -- and any context. Never looks through arrows or specified type variables.
177 -- Used for visible type application.
178 topInstantiateInferred :: CtOrigin -> TcSigmaType
179 -> TcM (HsWrapper, TcSigmaType)
180 -- if topInstantiate ty = (wrap, rho)
181 -- and e :: ty
182 -- then wrap e :: rho
183 topInstantiateInferred = top_instantiate False
184
185 top_instantiate :: Bool -- True <=> instantiate *all* variables
186 -- False <=> instantiate only the inferred ones
187 -> CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
188 top_instantiate inst_all orig ty
189 | not (null binders && null theta)
190 = do { let (inst_bndrs, leave_bndrs) = span should_inst binders
191 (inst_theta, leave_theta)
192 | null leave_bndrs = (theta, [])
193 | otherwise = ([], theta)
194 in_scope = mkInScopeSet (tyCoVarsOfType ty)
195 empty_subst = mkEmptyTCvSubst in_scope
196 inst_tvs = binderVars inst_bndrs
197 ; (subst, inst_tvs') <- mapAccumLM newMetaTyVarX empty_subst inst_tvs
198 ; let inst_theta' = substTheta subst inst_theta
199 sigma' = substTy subst (mkForAllTys leave_bndrs $
200 mkFunTys leave_theta rho)
201 inst_tv_tys' = mkTyVarTys inst_tvs'
202
203 ; wrap1 <- instCall orig inst_tv_tys' inst_theta'
204 ; traceTc "Instantiating"
205 (vcat [ text "all tyvars?" <+> ppr inst_all
206 , text "origin" <+> pprCtOrigin orig
207 , text "type" <+> debugPprType ty
208 , text "theta" <+> ppr theta
209 , text "leave_bndrs" <+> ppr leave_bndrs
210 , text "with" <+> vcat (map debugPprType inst_tv_tys')
211 , text "theta:" <+> ppr inst_theta' ])
212
213 ; (wrap2, rho2) <-
214 if null leave_bndrs
215
216 -- account for types like forall a. Num a => forall b. Ord b => ...
217 then top_instantiate inst_all orig sigma'
218
219 -- but don't loop if there were any un-inst'able tyvars
220 else return (idHsWrapper, sigma')
221
222 ; return (wrap2 <.> wrap1, rho2) }
223
224 | otherwise = return (idHsWrapper, ty)
225 where
226 (binders, phi) = tcSplitForAllVarBndrs ty
227 (theta, rho) = tcSplitPhiTy phi
228
229 should_inst bndr
230 | inst_all = True
231 | otherwise = binderArgFlag bndr == Inferred
232
233 deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
234 -- Int -> forall a. a -> a ==> (\x:Int. [] x alpha) :: Int -> alpha
235 -- In general if
236 -- if deeplyInstantiate ty = (wrap, rho)
237 -- and e :: ty
238 -- then wrap e :: rho
239 -- That is, wrap :: ty ~> rho
240 --
241 -- If you don't need the HsWrapper returned from this function, consider
242 -- using tcSplitNestedSigmaTys in TcType, which is a pure alternative that
243 -- only computes the returned TcRhoType.
244
245 deeplyInstantiate orig ty =
246 deeply_instantiate orig
247 (mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty)))
248 ty
249
250 deeply_instantiate :: CtOrigin
251 -> TCvSubst
252 -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
253 -- Internal function to deeply instantiate that builds on an existing subst.
254 -- It extends the input substitution and applies the final subtitution to
255 -- the types on return. See #12549.
256
257 deeply_instantiate orig subst ty
258 | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
259 = do { (subst', tvs') <- newMetaTyVarsX subst tvs
260 ; let arg_tys' = substTys subst' arg_tys
261 theta' = substTheta subst' theta
262 ; ids1 <- newSysLocalIds (fsLit "di") arg_tys'
263 ; wrap1 <- instCall orig (mkTyVarTys tvs') theta'
264 ; traceTc "Instantiating (deeply)" (vcat [ text "origin" <+> pprCtOrigin orig
265 , text "type" <+> ppr ty
266 , text "with" <+> ppr tvs'
267 , text "args:" <+> ppr ids1
268 , text "theta:" <+> ppr theta'
269 , text "subst:" <+> ppr subst'])
270 ; (wrap2, rho2) <- deeply_instantiate orig subst' rho
271 ; return (mkWpLams ids1
272 <.> wrap2
273 <.> wrap1
274 <.> mkWpEvVarApps ids1,
275 mkFunTys arg_tys' rho2) }
276
277 | otherwise
278 = do { let ty' = substTy subst ty
279 ; traceTc "deeply_instantiate final subst"
280 (vcat [ text "origin:" <+> pprCtOrigin orig
281 , text "type:" <+> ppr ty
282 , text "new type:" <+> ppr ty'
283 , text "subst:" <+> ppr subst ])
284 ; return (idHsWrapper, ty') }
285
286
287 instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst
288 -- Use this when you want to instantiate (forall a b c. ty) with
289 -- types [ta, tb, tc], but when the kinds of 'a' and 'ta' might
290 -- not yet match (perhaps because there are unsolved constraints; Trac #14154)
291 -- If they don't match, emit a kind-equality to promise that they will
292 -- eventually do so, and thus make a kind-homongeneous substitution.
293 instTyVarsWith orig tvs tys
294 = go empty_subst tvs tys
295 where
296 empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfTypes tys))
297
298 go subst [] []
299 = return subst
300 go subst (tv:tvs) (ty:tys)
301 | tv_kind `tcEqType` ty_kind
302 = go (extendTCvSubst subst tv ty) tvs tys
303 | otherwise
304 = do { co <- emitWantedEq orig KindLevel Nominal ty_kind tv_kind
305 ; go (extendTCvSubst subst tv (ty `mkCastTy` co)) tvs tys }
306 where
307 tv_kind = substTy subst (tyVarKind tv)
308 ty_kind = tcTypeKind ty
309
310 go _ _ _ = pprPanic "instTysWith" (ppr tvs $$ ppr tys)
311
312 {-
313 ************************************************************************
314 * *
315 Instantiating a call
316 * *
317 ************************************************************************
318
319 Note [Handling boxed equality]
320 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
321 The solver deals entirely in terms of unboxed (primitive) equality.
322 There should never be a boxed Wanted equality. Ever. But, what if
323 we are calling `foo :: forall a. (F a ~ Bool) => ...`? That equality
324 is boxed, so naive treatment here would emit a boxed Wanted equality.
325
326 So we simply check for this case and make the right boxing of evidence.
327
328 -}
329
330 ----------------
331 instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
332 -- Instantiate the constraints of a call
333 -- (instCall o tys theta)
334 -- (a) Makes fresh dictionaries as necessary for the constraints (theta)
335 -- (b) Throws these dictionaries into the LIE
336 -- (c) Returns an HsWrapper ([.] tys dicts)
337
338 instCall orig tys theta
339 = do { dict_app <- instCallConstraints orig theta
340 ; return (dict_app <.> mkWpTyApps tys) }
341
342 ----------------
343 instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
344 -- Instantiates the TcTheta, puts all constraints thereby generated
345 -- into the LIE, and returns a HsWrapper to enclose the call site.
346
347 instCallConstraints orig preds
348 | null preds
349 = return idHsWrapper
350 | otherwise
351 = do { evs <- mapM go preds
352 ; traceTc "instCallConstraints" (ppr evs)
353 ; return (mkWpEvApps evs) }
354 where
355 go :: TcPredType -> TcM EvTerm
356 go pred
357 | Just (Nominal, ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut #1
358 = do { co <- unifyType Nothing ty1 ty2
359 ; return (evCoercion co) }
360
361 -- Try short-cut #2
362 | Just (tc, args@[_, _, ty1, ty2]) <- splitTyConApp_maybe pred
363 , tc `hasKey` heqTyConKey
364 = do { co <- unifyType Nothing ty1 ty2
365 ; return (evDFunApp (dataConWrapId heqDataCon) args [Coercion co]) }
366
367 | otherwise
368 = emitWanted orig pred
369
370 instDFunType :: DFunId -> [DFunInstType]
371 -> TcM ( [TcType] -- instantiated argument types
372 , TcThetaType ) -- instantiated constraint
373 -- See Note [DFunInstType: instantiating types] in InstEnv
374 instDFunType dfun_id dfun_inst_tys
375 = do { (subst, inst_tys) <- go empty_subst dfun_tvs dfun_inst_tys
376 ; return (inst_tys, substTheta subst dfun_theta) }
377 where
378 dfun_ty = idType dfun_id
379 (dfun_tvs, dfun_theta, _) = tcSplitSigmaTy dfun_ty
380 empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType dfun_ty))
381 -- With quantified constraints, the
382 -- type of a dfun may not be closed
383
384 go :: TCvSubst -> [TyVar] -> [DFunInstType] -> TcM (TCvSubst, [TcType])
385 go subst [] [] = return (subst, [])
386 go subst (tv:tvs) (Just ty : mb_tys)
387 = do { (subst', tys) <- go (extendTvSubstAndInScope subst tv ty)
388 tvs
389 mb_tys
390 ; return (subst', ty : tys) }
391 go subst (tv:tvs) (Nothing : mb_tys)
392 = do { (subst', tv') <- newMetaTyVarX subst tv
393 ; (subst'', tys) <- go subst' tvs mb_tys
394 ; return (subst'', mkTyVarTy tv' : tys) }
395 go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr dfun_inst_tys)
396
397 ----------------
398 instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
399 -- Similar to instCall, but only emit the constraints in the LIE
400 -- Used exclusively for the 'stupid theta' of a data constructor
401 instStupidTheta orig theta
402 = do { _co <- instCallConstraints orig theta -- Discard the coercion
403 ; return () }
404
405 {-
406 ************************************************************************
407 * *
408 Instantiating Kinds
409 * *
410 ************************************************************************
411
412 Note [Constraints handled in types]
413 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
414 Generally, we cannot handle constraints written in types. For example,
415 if we declare
416
417 data C a where
418 MkC :: Show a => a -> C a
419
420 we will not be able to use MkC in types, as we have no way of creating
421 a type-level Show dictionary.
422
423 However, we make an exception for equality types. Consider
424
425 data T1 a where
426 MkT1 :: T1 Bool
427
428 data T2 a where
429 MkT2 :: a ~ Bool => T2 a
430
431 MkT1 has a constrained return type, while MkT2 uses an explicit equality
432 constraint. These two types are often written interchangeably, with a
433 reasonable expectation that they mean the same thing. For this to work --
434 and for us to be able to promote GADTs -- we need to be able to instantiate
435 equality constraints in types.
436
437 One wrinkle is that the equality in MkT2 is *lifted*. But, for proper
438 GADT equalities, GHC produces *unlifted* constraints. (This unlifting comes
439 from DataCon.eqSpecPreds, which uses mkPrimEqPred.) And, perhaps a wily
440 user will use (~~) for a heterogeneous equality. We thus must support
441 all of (~), (~~), and (~#) in types. (See Note [The equality types story]
442 in TysPrim for a primer on these equality types.)
443
444 The get_eq_tys_maybe function recognizes these three forms of equality,
445 returning a suitable type formation function and the two types related
446 by the equality constraint. In the lifted case, it uses mkHEqBoxTy or
447 mkEqBoxTy, which promote the datacons of the (~~) or (~) datatype,
448 respectively.
449
450 One might reasonably wonder who *unpacks* these boxes once they are
451 made. After all, there is no type-level `case` construct. The surprising
452 answer is that no one ever does. Instead, if a GADT constructor is used
453 on the left-hand side of a type family equation, that occurrence forces
454 GHC to unify the types in question. For example:
455
456 data G a where
457 MkG :: G Bool
458
459 type family F (x :: G a) :: a where
460 F MkG = False
461
462 When checking the LHS `F MkG`, GHC sees the MkG constructor and then must
463 unify F's implicit parameter `a` with Bool. This succeeds, making the equation
464
465 F Bool (MkG @Bool <Bool>) = False
466
467 Note that we never need unpack the coercion. This is because type family
468 equations are *not* parametric in their kind variables. That is, we could have
469 just said
470
471 type family H (x :: G a) :: a where
472 H _ = False
473
474 The presence of False on the RHS also forces `a` to become Bool, giving us
475
476 H Bool _ = False
477
478 The fact that any of this works stems from the lack of phase separation between
479 types and kinds (unlike the very present phase separation between terms and types).
480
481 Once we have the ability to pattern-match on types below top-level, this will
482 no longer cut it, but it seems fine for now.
483
484 -}
485
486 ---------------------------
487 -- | Instantantiate the TyConBinders of a forall type,
488 -- given its decomposed form (tvs, ty)
489 tcInstTyBinders :: HasDebugCallStack
490 => ([TyCoBinder], TcKind) -- ^ The type (forall bs. ty)
491 -> TcM ([TcType], TcKind) -- ^ Instantiated bs, substituted ty
492 -- Takes a pair because that is what splitPiTysInvisible returns
493 -- See also Note [Bidirectional type checking]
494 tcInstTyBinders (bndrs, ty)
495 | null bndrs -- It's fine for bndrs to be empty e.g.
496 = return ([], ty) -- Check that (Maybe :: forall {k}. k->*),
497 -- and see the call to instTyBinders in checkExpectedKind
498 -- A user bug to be reported as such; it is not a compiler crash!
499
500 | otherwise
501 = do { (subst, args) <- mapAccumLM (tcInstTyBinder Nothing) empty_subst bndrs
502 ; ty' <- zonkTcType (substTy subst ty)
503 -- Why zonk the result? So that tcTyVar can
504 -- obey (IT6) of Note [The tcType invariant] in TcHsType
505 -- ToDo: SLPJ: I don't think this is needed
506 ; return (args, ty') }
507 where
508 empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
509
510 -- | Used only in *types*
511 tcInstTyBinder :: Maybe (VarEnv Kind)
512 -> TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
513 tcInstTyBinder mb_kind_info subst (Named (Bndr tv _))
514 = case lookup_tv tv of
515 Just ki -> return (extendTvSubstAndInScope subst tv ki, ki)
516 Nothing -> do { (subst', tv') <- newMetaTyVarX subst tv
517 ; return (subst', mkTyVarTy tv') }
518 where
519 lookup_tv tv = do { env <- mb_kind_info -- `Maybe` monad
520 ; lookupVarEnv env tv }
521
522
523 tcInstTyBinder _ subst (Anon ty)
524 -- This is the *only* constraint currently handled in types.
525 | Just (mk, k1, k2) <- get_eq_tys_maybe substed_ty
526 = do { co <- unifyKind Nothing k1 k2
527 ; arg' <- mk co
528 ; return (subst, arg') }
529
530 | isPredTy substed_ty
531 = do { let (env, tidy_ty) = tidyOpenType emptyTidyEnv substed_ty
532 ; addErrTcM (env, text "Illegal constraint in a kind:" <+> ppr tidy_ty)
533
534 -- just invent a new variable so that we can continue
535 ; u <- newUnique
536 ; let name = mkSysTvName u (fsLit "dict")
537 ; return (subst, mkTyVarTy $ mkTyVar name substed_ty) }
538
539
540 | otherwise
541 = do { tv_ty <- newFlexiTyVarTy substed_ty
542 ; return (subst, tv_ty) }
543
544 where
545 substed_ty = substTy subst ty
546
547 -- See Note [Constraints handled in types]
548 get_eq_tys_maybe :: Type
549 -> Maybe ( Coercion -> TcM Type
550 -- given a coercion proving t1 ~# t2, produce the
551 -- right instantiation for the TyBinder at hand
552 , Type -- t1
553 , Type -- t2
554 )
555 get_eq_tys_maybe ty
556 -- unlifted equality (~#)
557 | Just (Nominal, k1, k2) <- getEqPredTys_maybe ty
558 = Just (\co -> return $ mkCoercionTy co, k1, k2)
559
560 -- lifted heterogeneous equality (~~)
561 | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
562 = if | tc `hasKey` heqTyConKey
563 -> Just (\co -> mkHEqBoxTy co k1 k2, k1, k2)
564 | otherwise
565 -> Nothing
566
567 -- lifted homogeneous equality (~)
568 | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
569 = if | tc `hasKey` eqTyConKey
570 -> Just (\co -> mkEqBoxTy co k1 k2, k1, k2)
571 | otherwise
572 -> Nothing
573
574 | otherwise
575 = Nothing
576
577 -------------------------------
578 -- | This takes @a ~# b@ and returns @a ~~ b@.
579 mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
580 -- monadic just for convenience with mkEqBoxTy
581 mkHEqBoxTy co ty1 ty2
582 = return $
583 mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
584 where k1 = tcTypeKind ty1
585 k2 = tcTypeKind ty2
586
587 -- | This takes @a ~# b@ and returns @a ~ b@.
588 mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
589 mkEqBoxTy co ty1 ty2
590 = return $
591 mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
592 where k = tcTypeKind ty1
593
594 {-
595 ************************************************************************
596 * *
597 Literals
598 * *
599 ************************************************************************
600
601 -}
602
603 {-
604 In newOverloadedLit we convert directly to an Int or Integer if we
605 know that's what we want. This may save some time, by not
606 temporarily generating overloaded literals, but it won't catch all
607 cases (the rest are caught in lookupInst).
608
609 -}
610
611 newOverloadedLit :: HsOverLit GhcRn
612 -> ExpRhoType
613 -> TcM (HsOverLit GhcTcId)
614 newOverloadedLit
615 lit@(OverLit { ol_val = val, ol_ext = rebindable }) res_ty
616 | not rebindable
617 -- all built-in overloaded lits are tau-types, so we can just
618 -- tauify the ExpType
619 = do { res_ty <- expTypeToType res_ty
620 ; dflags <- getDynFlags
621 ; case shortCutLit dflags val res_ty of
622 -- Do not generate a LitInst for rebindable syntax.
623 -- Reason: If we do, tcSimplify will call lookupInst, which
624 -- will call tcSyntaxName, which does unification,
625 -- which tcSimplify doesn't like
626 Just expr -> return (lit { ol_witness = expr
627 , ol_ext = OverLitTc False res_ty })
628 Nothing -> newNonTrivialOverloadedLit orig lit
629 (mkCheckExpType res_ty) }
630
631 | otherwise
632 = newNonTrivialOverloadedLit orig lit res_ty
633 where
634 orig = LiteralOrigin lit
635 newOverloadedLit XOverLit{} _ = panic "newOverloadedLit"
636
637 -- Does not handle things that 'shortCutLit' can handle. See also
638 -- newOverloadedLit in TcUnify
639 newNonTrivialOverloadedLit :: CtOrigin
640 -> HsOverLit GhcRn
641 -> ExpRhoType
642 -> TcM (HsOverLit GhcTcId)
643 newNonTrivialOverloadedLit orig
644 lit@(OverLit { ol_val = val, ol_witness = HsVar _ (L _ meth_name)
645 , ol_ext = rebindable }) res_ty
646 = do { hs_lit <- mkOverLit val
647 ; let lit_ty = hsLitType hs_lit
648 ; (_, fi') <- tcSyntaxOp orig (mkRnSyntaxExpr meth_name)
649 [synKnownType lit_ty] res_ty $
650 \_ -> return ()
651 ; let L _ witness = nlHsSyntaxApps fi' [nlHsLit hs_lit]
652 ; res_ty <- readExpType res_ty
653 ; return (lit { ol_witness = witness
654 , ol_ext = OverLitTc rebindable res_ty }) }
655 newNonTrivialOverloadedLit _ lit _
656 = pprPanic "newNonTrivialOverloadedLit" (ppr lit)
657
658 ------------
659 mkOverLit ::OverLitVal -> TcM (HsLit GhcTc)
660 mkOverLit (HsIntegral i)
661 = do { integer_ty <- tcMetaTy integerTyConName
662 ; return (HsInteger (il_text i)
663 (il_value i) integer_ty) }
664
665 mkOverLit (HsFractional r)
666 = do { rat_ty <- tcMetaTy rationalTyConName
667 ; return (HsRat noExt r rat_ty) }
668
669 mkOverLit (HsIsString src s) = return (HsString src s)
670
671 {-
672 ************************************************************************
673 * *
674 Re-mappable syntax
675
676 Used only for arrow syntax -- find a way to nuke this
677 * *
678 ************************************************************************
679
680 Suppose we are doing the -XRebindableSyntax thing, and we encounter
681 a do-expression. We have to find (>>) in the current environment, which is
682 done by the rename. Then we have to check that it has the same type as
683 Control.Monad.(>>). Or, more precisely, a compatible type. One 'customer' had
684 this:
685
686 (>>) :: HB m n mn => m a -> n b -> mn b
687
688 So the idea is to generate a local binding for (>>), thus:
689
690 let then72 :: forall a b. m a -> m b -> m b
691 then72 = ...something involving the user's (>>)...
692 in
693 ...the do-expression...
694
695 Now the do-expression can proceed using then72, which has exactly
696 the expected type.
697
698 In fact tcSyntaxName just generates the RHS for then72, because we only
699 want an actual binding in the do-expression case. For literals, we can
700 just use the expression inline.
701 -}
702
703 tcSyntaxName :: CtOrigin
704 -> TcType -- ^ Type to instantiate it at
705 -> (Name, HsExpr GhcRn) -- ^ (Standard name, user name)
706 -> TcM (Name, HsExpr GhcTcId)
707 -- ^ (Standard name, suitable expression)
708 -- USED ONLY FOR CmdTop (sigh) ***
709 -- See Note [CmdSyntaxTable] in HsExpr
710
711 tcSyntaxName orig ty (std_nm, HsVar _ (L _ user_nm))
712 | std_nm == user_nm
713 = do rhs <- newMethodFromName orig std_nm ty
714 return (std_nm, rhs)
715
716 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
717 std_id <- tcLookupId std_nm
718 let
719 -- C.f. newMethodAtLoc
720 ([tv], _, tau) = tcSplitSigmaTy (idType std_id)
721 sigma1 = substTyWith [tv] [ty] tau
722 -- Actually, the "tau-type" might be a sigma-type in the
723 -- case of locally-polymorphic methods.
724
725 addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
726
727 -- Check that the user-supplied thing has the
728 -- same type as the standard one.
729 -- Tiresome jiggling because tcCheckSigma takes a located expression
730 span <- getSrcSpanM
731 expr <- tcPolyExpr (L span user_nm_expr) sigma1
732 return (std_nm, unLoc expr)
733
734 syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> TidyEnv
735 -> TcRn (TidyEnv, SDoc)
736 syntaxNameCtxt name orig ty tidy_env
737 = do { inst_loc <- getCtLocM orig (Just TypeLevel)
738 ; let msg = vcat [ text "When checking that" <+> quotes (ppr name)
739 <+> text "(needed by a syntactic construct)"
740 , nest 2 (text "has the required type:"
741 <+> ppr (tidyType tidy_env ty))
742 , nest 2 (pprCtLoc inst_loc) ]
743 ; return (tidy_env, msg) }
744
745 {-
746 ************************************************************************
747 * *
748 Instances
749 * *
750 ************************************************************************
751 -}
752
753 getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
754 -- Construct the OverlapFlag from the global module flags,
755 -- but if the overlap_mode argument is (Just m),
756 -- set the OverlapMode to 'm'
757 getOverlapFlag overlap_mode
758 = do { dflags <- getDynFlags
759 ; let overlap_ok = xopt LangExt.OverlappingInstances dflags
760 incoherent_ok = xopt LangExt.IncoherentInstances dflags
761 use x = OverlapFlag { isSafeOverlap = safeLanguageOn dflags
762 , overlapMode = x }
763 default_oflag | incoherent_ok = use (Incoherent NoSourceText)
764 | overlap_ok = use (Overlaps NoSourceText)
765 | otherwise = use (NoOverlap NoSourceText)
766
767 final_oflag = setOverlapModeMaybe default_oflag overlap_mode
768 ; return final_oflag }
769
770 tcGetInsts :: TcM [ClsInst]
771 -- Gets the local class instances.
772 tcGetInsts = fmap tcg_insts getGblEnv
773
774 newClsInst :: Maybe OverlapMode -> Name -> [TyVar] -> ThetaType
775 -> Class -> [Type] -> TcM ClsInst
776 newClsInst overlap_mode dfun_name tvs theta clas tys
777 = do { (subst, tvs') <- freshenTyVarBndrs tvs
778 -- Be sure to freshen those type variables,
779 -- so they are sure not to appear in any lookup
780 ; let tys' = substTys subst tys
781
782 dfun = mkDictFunId dfun_name tvs theta clas tys
783 -- The dfun uses the original 'tvs' because
784 -- (a) they don't need to be fresh
785 -- (b) they may be mentioned in the ib_binds field of
786 -- an InstInfo, and in TcEnv.pprInstInfoDetails it's
787 -- helpful to use the same names
788
789 ; oflag <- getOverlapFlag overlap_mode
790 ; let inst = mkLocalInstance dfun oflag tvs' clas tys'
791 ; warnIfFlag Opt_WarnOrphans
792 (isOrphan (is_orphan inst))
793 (instOrphWarn inst)
794 ; return inst }
795
796 instOrphWarn :: ClsInst -> SDoc
797 instOrphWarn inst
798 = hang (text "Orphan instance:") 2 (pprInstanceHdr inst)
799 $$ text "To avoid this"
800 $$ nest 4 (vcat possibilities)
801 where
802 possibilities =
803 text "move the instance declaration to the module of the class or of the type, or" :
804 text "wrap the type with a newtype and declare the instance on the new type." :
805 []
806
807 tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
808 -- Add new locally-defined instances
809 tcExtendLocalInstEnv dfuns thing_inside
810 = do { traceDFuns dfuns
811 ; env <- getGblEnv
812 ; (inst_env', cls_insts') <- foldlM addLocalInst
813 (tcg_inst_env env, tcg_insts env)
814 dfuns
815 ; let env' = env { tcg_insts = cls_insts'
816 , tcg_inst_env = inst_env' }
817 ; setGblEnv env' thing_inside }
818
819 addLocalInst :: (InstEnv, [ClsInst]) -> ClsInst -> TcM (InstEnv, [ClsInst])
820 -- Check that the proposed new instance is OK,
821 -- and then add it to the home inst env
822 -- If overwrite_inst, then we can overwrite a direct match
823 addLocalInst (home_ie, my_insts) ispec
824 = do {
825 -- Load imported instances, so that we report
826 -- duplicates correctly
827
828 -- 'matches' are existing instance declarations that are less
829 -- specific than the new one
830 -- 'dups' are those 'matches' that are equal to the new one
831 ; isGHCi <- getIsGHCi
832 ; eps <- getEps
833 ; tcg_env <- getGblEnv
834
835 -- In GHCi, we *override* any identical instances
836 -- that are also defined in the interactive context
837 -- See Note [Override identical instances in GHCi]
838 ; let home_ie'
839 | isGHCi = deleteFromInstEnv home_ie ispec
840 | otherwise = home_ie
841
842 global_ie = eps_inst_env eps
843 inst_envs = InstEnvs { ie_global = global_ie
844 , ie_local = home_ie'
845 , ie_visible = tcVisibleOrphanMods tcg_env }
846
847 -- Check for inconsistent functional dependencies
848 ; let inconsistent_ispecs = checkFunDeps inst_envs ispec
849 ; unless (null inconsistent_ispecs) $
850 funDepErr ispec inconsistent_ispecs
851
852 -- Check for duplicate instance decls.
853 ; let (_tvs, cls, tys) = instanceHead ispec
854 (matches, _, _) = lookupInstEnv False inst_envs cls tys
855 dups = filter (identicalClsInstHead ispec) (map fst matches)
856 ; unless (null dups) $
857 dupInstErr ispec (head dups)
858
859 ; return (extendInstEnv home_ie' ispec, ispec : my_insts) }
860
861 {-
862 Note [Signature files and type class instances]
863 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
864 Instances in signature files do not have an effect when compiling:
865 when you compile a signature against an implementation, you will
866 see the instances WHETHER OR NOT the instance is declared in
867 the file (this is because the signatures go in the EPS and we
868 can't filter them out easily.) This is also why we cannot
869 place the instance in the hi file: it would show up as a duplicate,
870 and we don't have instance reexports anyway.
871
872 However, you might find them useful when typechecking against
873 a signature: the instance is a way of indicating to GHC that
874 some instance exists, in case downstream code uses it.
875
876 Implementing this is a little tricky. Consider the following
877 situation (sigof03):
878
879 module A where
880 instance C T where ...
881
882 module ASig where
883 instance C T
884
885 When compiling ASig, A.hi is loaded, which brings its instances
886 into the EPS. When we process the instance declaration in ASig,
887 we should ignore it for the purpose of doing a duplicate check,
888 since it's not actually a duplicate. But don't skip the check
889 entirely, we still want this to fail (tcfail221):
890
891 module ASig where
892 instance C T
893 instance C T
894
895 Note that in some situations, the interface containing the type
896 class instances may not have been loaded yet at all. The usual
897 situation when A imports another module which provides the
898 instances (sigof02m):
899
900 module A(module B) where
901 import B
902
903 See also Note [Signature lazy interface loading]. We can't
904 rely on this, however, since sometimes we'll have spurious
905 type class instances in the EPS, see #9422 (sigof02dm)
906
907 ************************************************************************
908 * *
909 Errors and tracing
910 * *
911 ************************************************************************
912 -}
913
914 traceDFuns :: [ClsInst] -> TcRn ()
915 traceDFuns ispecs
916 = traceTc "Adding instances:" (vcat (map pp ispecs))
917 where
918 pp ispec = hang (ppr (instanceDFunId ispec) <+> colon)
919 2 (ppr ispec)
920 -- Print the dfun name itself too
921
922 funDepErr :: ClsInst -> [ClsInst] -> TcRn ()
923 funDepErr ispec ispecs
924 = addClsInstsErr (text "Functional dependencies conflict between instance declarations:")
925 (ispec : ispecs)
926
927 dupInstErr :: ClsInst -> ClsInst -> TcRn ()
928 dupInstErr ispec dup_ispec
929 = addClsInstsErr (text "Duplicate instance declarations:")
930 [ispec, dup_ispec]
931
932 addClsInstsErr :: SDoc -> [ClsInst] -> TcRn ()
933 addClsInstsErr herald ispecs
934 = setSrcSpan (getSrcSpan (head sorted)) $
935 addErr (hang herald 2 (pprInstances sorted))
936 where
937 sorted = sortWith getSrcLoc ispecs
938 -- The sortWith just arranges that instances are dislayed in order
939 -- of source location, which reduced wobbling in error messages,
940 -- and is better for users