never executed always true always false
1
2 {-# LANGUAGE FlexibleContexts #-}
3 {-# LANGUAGE DisambiguateRecordFields #-}
4
5 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
6 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
7
8 {-
9 (c) The University of Glasgow 2006
10 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
11
12 -}
13
14 module GHC.Tc.Utils.Instantiate (
15 topSkolemise,
16 topInstantiate,
17 instantiateSigma,
18 instCall, instDFunType, instStupidTheta, instTyVarsWith,
19 newWanted, newWanteds,
20
21 tcInstType, tcInstTypeBndrs,
22 tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
23 tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
24
25 freshenTyVarBndrs, freshenCoVarBndrsX,
26
27 tcInstInvisibleTyBindersN, tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,
28
29 newOverloadedLit, mkOverLit,
30
31 newClsInst,
32 tcGetInsts, tcGetInstEnvs, getOverlapFlag,
33 tcExtendLocalInstEnv,
34 instCallConstraints, newMethodFromName,
35 tcSyntaxName,
36
37 -- Simple functions over evidence variables
38 tyCoVarsOfWC,
39 tyCoVarsOfCt, tyCoVarsOfCts,
40 ) where
41
42 import GHC.Prelude
43
44 import GHC.Driver.Session
45 import GHC.Driver.Env
46
47 import GHC.Builtin.Types ( heqDataCon, eqDataCon, integerTyConName )
48 import GHC.Builtin.Names
49
50 import GHC.Hs
51 import GHC.Hs.Syn.Type ( hsLitType )
52
53 import GHC.Core.InstEnv
54 import GHC.Core.Predicate
55 import GHC.Core ( Expr(..), isOrphan ) -- For the Coercion constructor
56 import GHC.Core.Type
57 import GHC.Core.Multiplicity
58 import GHC.Core.TyCo.Rep
59 import GHC.Core.TyCo.Ppr ( debugPprType )
60 import GHC.Core.Class( Class )
61 import GHC.Core.DataCon
62
63 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcCheckPolyExpr, tcSyntaxOp )
64 import {-# SOURCE #-} GHC.Tc.Utils.Unify( unifyType, unifyKind )
65 import GHC.Tc.Utils.Zonk
66 import GHC.Tc.Utils.Monad
67 import GHC.Tc.Types.Constraint
68 import GHC.Tc.Types.Origin
69 import GHC.Tc.Utils.Env
70 import GHC.Tc.Types.Evidence
71 import GHC.Tc.Instance.FunDeps
72 import GHC.Tc.Utils.Concrete
73 import GHC.Tc.Utils.TcMType
74 import GHC.Tc.Utils.TcType
75 import GHC.Tc.Errors.Types
76
77 import GHC.Types.Id.Make( mkDictFunId )
78 import GHC.Types.Basic ( TypeOrKind(..), Arity )
79 import GHC.Types.Error
80 import GHC.Types.SourceText
81 import GHC.Types.SrcLoc as SrcLoc
82 import GHC.Types.Var.Env
83 import GHC.Types.Var.Set
84 import GHC.Types.Id
85 import GHC.Types.Name
86 import GHC.Types.Var
87 import qualified GHC.LanguageExtensions as LangExt
88
89 import GHC.Utils.Misc
90 import GHC.Utils.Panic
91 import GHC.Utils.Panic.Plain
92 import GHC.Utils.Outputable
93
94 import GHC.Unit.State
95 import GHC.Unit.External
96
97 import Data.List ( mapAccumL )
98 import qualified Data.List.NonEmpty as NE
99 import Control.Monad( when, unless, void )
100 import Data.Function ( on )
101
102 {-
103 ************************************************************************
104 * *
105 Creating and emittind constraints
106 * *
107 ************************************************************************
108 -}
109
110 newMethodFromName
111 :: CtOrigin -- ^ why do we need this?
112 -> Name -- ^ name of the method
113 -> [TcRhoType] -- ^ types with which to instantiate the class
114 -> TcM (HsExpr GhcTc)
115 -- ^ Used when 'Name' is the wired-in name for a wired-in class method,
116 -- so the caller knows its type for sure, which should be of form
117 --
118 -- > forall a. C a => <blah>
119 --
120 -- 'newMethodFromName' is supposed to instantiate just the outer
121 -- type variable and constraint
122
123 newMethodFromName origin name ty_args
124 = do { id <- tcLookupId name
125 -- Use tcLookupId not tcLookupGlobalId; the method is almost
126 -- always a class op, but with -XRebindableSyntax GHC is
127 -- meant to find whatever thing is in scope, and that may
128 -- be an ordinary function.
129
130 ; let ty = piResultTys (idType id) ty_args
131 (theta, _caller_knows_this) = tcSplitPhiTy ty
132 ; wrap <- assert (not (isForAllTy ty) && isSingleton theta) $
133 instCall origin ty_args theta
134
135 ; return (mkHsWrap wrap (HsVar noExtField (noLocA id))) }
136
137 {-
138 ************************************************************************
139 * *
140 Instantiation and skolemisation
141 * *
142 ************************************************************************
143
144 Note [Skolemisation]
145 ~~~~~~~~~~~~~~~~~~~~
146 topSkolemise decomposes and skolemises a type, returning a type
147 with no top level foralls or (=>)
148
149 Examples:
150
151 topSkolemise (forall a. Ord a => a -> a)
152 = ( wp, [a], [d:Ord a], a->a )
153 where wp = /\a. \(d:Ord a). <hole> a d
154
155 topSkolemise (forall a. Ord a => forall b. Eq b => a->b->b)
156 = ( wp, [a,b], [d1:Ord a,d2:Eq b], a->b->b )
157 where wp = /\a.\(d1:Ord a)./\b.\(d2:Ord b). <hole> a d1 b d2
158
159 This second example is the reason for the recursive 'go'
160 function in topSkolemise: we must remove successive layers
161 of foralls and (=>).
162
163 In general,
164 if topSkolemise ty = (wrap, tvs, evs, rho)
165 and e :: rho
166 then wrap e :: ty
167 and 'wrap' binds {tvs, evs}
168
169 -}
170
171 topSkolemise :: TcSigmaType
172 -> TcM ( HsWrapper
173 , [(Name,TyVar)] -- All skolemised variables
174 , [EvVar] -- All "given"s
175 , TcRhoType )
176 -- See Note [Skolemisation]
177 topSkolemise ty
178 = go init_subst idHsWrapper [] [] ty
179 where
180 init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
181
182 -- Why recursive? See Note [Skolemisation]
183 go subst wrap tv_prs ev_vars ty
184 | (tvs, theta, inner_ty) <- tcSplitSigmaTy ty
185 , not (null tvs && null theta)
186 = do { (subst', tvs1) <- tcInstSkolTyVarsX subst tvs
187 ; ev_vars1 <- newEvVars (substTheta subst' theta)
188 ; go subst'
189 (wrap <.> mkWpTyLams tvs1 <.> mkWpLams ev_vars1)
190 (tv_prs ++ (map tyVarName tvs `zip` tvs1))
191 (ev_vars ++ ev_vars1)
192 inner_ty }
193
194 | otherwise
195 = return (wrap, tv_prs, ev_vars, substTy subst ty)
196 -- substTy is a quick no-op on an empty substitution
197
198 topInstantiate ::CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
199 -- Instantiate outer invisible binders (both Inferred and Specified)
200 -- If top_instantiate ty = (wrap, inner_ty)
201 -- then wrap :: inner_ty "->" ty
202 -- NB: returns a type with no (=>),
203 -- and no invisible forall at the top
204 topInstantiate orig sigma
205 | (tvs, body1) <- tcSplitSomeForAllTyVars isInvisibleArgFlag sigma
206 , (theta, body2) <- tcSplitPhiTy body1
207 , not (null tvs && null theta)
208 = do { (_, wrap1, body3) <- instantiateSigma orig tvs theta body2
209
210 -- Loop, to account for types like
211 -- forall a. Num a => forall b. Ord b => ...
212 ; (wrap2, body4) <- topInstantiate orig body3
213
214 ; return (wrap2 <.> wrap1, body4) }
215
216 | otherwise = return (idHsWrapper, sigma)
217
218 instantiateSigma :: CtOrigin -> [TyVar] -> TcThetaType -> TcSigmaType
219 -> TcM ([TcTyVar], HsWrapper, TcSigmaType)
220 -- (instantiate orig tvs theta ty)
221 -- instantiates the the type variables tvs, emits the (instantiated)
222 -- constraints theta, and returns the (instantiated) type ty
223 instantiateSigma orig tvs theta body_ty
224 = do { (subst, inst_tvs) <- mapAccumLM newMetaTyVarX empty_subst tvs
225 ; let inst_theta = substTheta subst theta
226 inst_body = substTy subst body_ty
227 inst_tv_tys = mkTyVarTys inst_tvs
228
229 ; wrap <- instCall orig inst_tv_tys inst_theta
230 ; traceTc "Instantiating"
231 (vcat [ text "origin" <+> pprCtOrigin orig
232 , text "tvs" <+> ppr tvs
233 , text "theta" <+> ppr theta
234 , text "type" <+> debugPprType body_ty
235 , text "with" <+> vcat (map debugPprType inst_tv_tys)
236 , text "theta:" <+> ppr inst_theta ])
237
238 ; return (inst_tvs, wrap, inst_body) }
239 where
240 free_tvs = tyCoVarsOfType body_ty `unionVarSet` tyCoVarsOfTypes theta
241 in_scope = mkInScopeSet (free_tvs `delVarSetList` tvs)
242 empty_subst = mkEmptyTCvSubst in_scope
243
244 instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst
245 -- Use this when you want to instantiate (forall a b c. ty) with
246 -- types [ta, tb, tc], but when the kinds of 'a' and 'ta' might
247 -- not yet match (perhaps because there are unsolved constraints; #14154)
248 -- If they don't match, emit a kind-equality to promise that they will
249 -- eventually do so, and thus make a kind-homongeneous substitution.
250 instTyVarsWith orig tvs tys
251 = go emptyTCvSubst tvs tys
252 where
253 go subst [] []
254 = return subst
255 go subst (tv:tvs) (ty:tys)
256 | tv_kind `tcEqType` ty_kind
257 = go (extendTvSubstAndInScope subst tv ty) tvs tys
258 | otherwise
259 = do { co <- emitWantedEq orig KindLevel Nominal ty_kind tv_kind
260 ; go (extendTvSubstAndInScope subst tv (ty `mkCastTy` co)) tvs tys }
261 where
262 tv_kind = substTy subst (tyVarKind tv)
263 ty_kind = tcTypeKind ty
264
265 go _ _ _ = pprPanic "instTysWith" (ppr tvs $$ ppr tys)
266
267
268 {-
269 ************************************************************************
270 * *
271 Instantiating a call
272 * *
273 ************************************************************************
274
275 Note [Handling boxed equality]
276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
277 The solver deals entirely in terms of unboxed (primitive) equality.
278 There should never be a boxed Wanted equality. Ever. But, what if
279 we are calling `foo :: forall a. (F a ~ Bool) => ...`? That equality
280 is boxed, so naive treatment here would emit a boxed Wanted equality.
281
282 So we simply check for this case and make the right boxing of evidence.
283
284 -}
285
286 ----------------
287 instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
288 -- Instantiate the constraints of a call
289 -- (instCall o tys theta)
290 -- (a) Makes fresh dictionaries as necessary for the constraints (theta)
291 -- (b) Throws these dictionaries into the LIE
292 -- (c) Returns an HsWrapper ([.] tys dicts)
293
294 instCall orig tys theta
295 = do { dict_app <- instCallConstraints orig theta
296 ; return (dict_app <.> mkWpTyApps tys) }
297
298 ----------------
299 instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
300 -- Instantiates the TcTheta, puts all constraints thereby generated
301 -- into the LIE, and returns a HsWrapper to enclose the call site.
302
303 instCallConstraints orig preds
304 | null preds
305 = return idHsWrapper
306 | otherwise
307 = do { evs <- mapM go preds
308 ; traceTc "instCallConstraints" (ppr evs)
309 ; return (mkWpEvApps evs) }
310 where
311 go :: TcPredType -> TcM EvTerm
312 go pred
313 | Just (Nominal, ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut #1
314 = do { co <- unifyType Nothing ty1 ty2
315 ; return (evCoercion co) }
316
317 -- Try short-cut #2
318 | Just (tc, args@[_, _, ty1, ty2]) <- splitTyConApp_maybe pred
319 , tc `hasKey` heqTyConKey
320 = do { co <- unifyType Nothing ty1 ty2
321 ; return (evDFunApp (dataConWrapId heqDataCon) args [Coercion co]) }
322
323 | otherwise
324 = emitWanted orig pred
325
326 instDFunType :: DFunId -> [DFunInstType]
327 -> TcM ( [TcType] -- instantiated argument types
328 , TcThetaType ) -- instantiated constraint
329 -- See Note [DFunInstType: instantiating types] in GHC.Core.InstEnv
330 instDFunType dfun_id dfun_inst_tys
331 = do { (subst, inst_tys) <- go empty_subst dfun_tvs dfun_inst_tys
332 ; return (inst_tys, substTheta subst dfun_theta) }
333 where
334 dfun_ty = idType dfun_id
335 (dfun_tvs, dfun_theta, _) = tcSplitSigmaTy dfun_ty
336 empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType dfun_ty))
337 -- With quantified constraints, the
338 -- type of a dfun may not be closed
339
340 go :: TCvSubst -> [TyVar] -> [DFunInstType] -> TcM (TCvSubst, [TcType])
341 go subst [] [] = return (subst, [])
342 go subst (tv:tvs) (Just ty : mb_tys)
343 = do { (subst', tys) <- go (extendTvSubstAndInScope subst tv ty)
344 tvs
345 mb_tys
346 ; return (subst', ty : tys) }
347 go subst (tv:tvs) (Nothing : mb_tys)
348 = do { (subst', tv') <- newMetaTyVarX subst tv
349 ; (subst'', tys) <- go subst' tvs mb_tys
350 ; return (subst'', mkTyVarTy tv' : tys) }
351 go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr dfun_inst_tys)
352
353 ----------------
354 instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
355 -- Similar to instCall, but only emit the constraints in the LIE
356 -- Used exclusively for the 'stupid theta' of a data constructor
357 instStupidTheta orig theta
358 = do { _co <- instCallConstraints orig theta -- Discard the coercion
359 ; return () }
360
361
362 {- *********************************************************************
363 * *
364 Instantiating Kinds
365 * *
366 ********************************************************************* -}
367
368 -- | Given ty::forall k1 k2. k, instantiate all the invisible forall-binders
369 -- returning ty @kk1 @kk2 :: k[kk1/k1, kk2/k1]
370 tcInstInvisibleTyBinders :: TcType -> TcKind -> TcM (TcType, TcKind)
371 tcInstInvisibleTyBinders ty kind
372 = do { (extra_args, kind') <- tcInstInvisibleTyBindersN n_invis kind
373 ; return (mkAppTys ty extra_args, kind') }
374 where
375 n_invis = invisibleTyBndrCount kind
376
377 tcInstInvisibleTyBindersN :: Int -> TcKind -> TcM ([TcType], TcKind)
378 tcInstInvisibleTyBindersN 0 kind
379 = return ([], kind)
380 tcInstInvisibleTyBindersN n ty
381 = go n empty_subst ty
382 where
383 empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
384
385 go n subst kind
386 | n > 0
387 , Just (bndr, body) <- tcSplitPiTy_maybe kind
388 , isInvisibleBinder bndr
389 = do { (subst', arg) <- tcInstInvisibleTyBinder subst bndr
390 ; (args, inner_ty) <- go (n-1) subst' body
391 ; return (arg:args, inner_ty) }
392 | otherwise
393 = return ([], substTy subst kind)
394
395 -- | Used only in *types*
396 tcInstInvisibleTyBinder :: TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
397 tcInstInvisibleTyBinder subst (Named (Bndr tv _))
398 = do { (subst', tv') <- newMetaTyVarX subst tv
399 ; return (subst', mkTyVarTy tv') }
400
401 tcInstInvisibleTyBinder subst (Anon af ty)
402 | Just (mk, k1, k2) <- get_eq_tys_maybe (substTy subst (scaledThing ty))
403 -- Equality is the *only* constraint currently handled in types.
404 -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
405 = assert (af == InvisArg) $
406 do { co <- unifyKind Nothing k1 k2
407 ; arg' <- mk co
408 ; return (subst, arg') }
409
410 | otherwise -- This should never happen
411 -- See GHC.Core.TyCo.Rep Note [Constraints in kinds]
412 = pprPanic "tcInvisibleTyBinder" (ppr ty)
413
414 -------------------------------
415 get_eq_tys_maybe :: Type
416 -> Maybe ( Coercion -> TcM Type
417 -- given a coercion proving t1 ~# t2, produce the
418 -- right instantiation for the TyBinder at hand
419 , Type -- t1
420 , Type -- t2
421 )
422 -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
423 get_eq_tys_maybe ty
424 -- Lifted heterogeneous equality (~~)
425 | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
426 , tc `hasKey` heqTyConKey
427 = Just (\co -> mkHEqBoxTy co k1 k2, k1, k2)
428
429 -- Lifted homogeneous equality (~)
430 | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
431 , tc `hasKey` eqTyConKey
432 = Just (\co -> mkEqBoxTy co k1 k2, k1, k2)
433
434 | otherwise
435 = Nothing
436
437 -- | This takes @a ~# b@ and returns @a ~~ b@.
438 mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
439 -- monadic just for convenience with mkEqBoxTy
440 mkHEqBoxTy co ty1 ty2
441 = return $
442 mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
443 where k1 = tcTypeKind ty1
444 k2 = tcTypeKind ty2
445
446 -- | This takes @a ~# b@ and returns @a ~ b@.
447 mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
448 mkEqBoxTy co ty1 ty2
449 = return $
450 mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
451 where k = tcTypeKind ty1
452
453 {- *********************************************************************
454 * *
455 SkolemTvs (immutable)
456 * *
457 ********************************************************************* -}
458
459 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
460 -- ^ How to instantiate the type variables
461 -> Id -- ^ Type to instantiate
462 -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
463 -- (type vars, preds (incl equalities), rho)
464 tcInstType inst_tyvars id
465 | null tyvars -- There may be overloading despite no type variables;
466 -- (?x :: Int) => Int -> Int
467 = return ([], theta, tau)
468 | otherwise
469 = do { (subst, tyvars') <- inst_tyvars tyvars
470 ; let tv_prs = map tyVarName tyvars `zip` tyvars'
471 subst' = extendTCvInScopeSet subst (tyCoVarsOfType rho)
472 ; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
473 where
474 (tyvars, rho) = tcSplitForAllInvisTyVars (idType id)
475 (theta, tau) = tcSplitPhiTy rho
476
477 tcInstTypeBndrs :: Id -> TcM ([(Name, InvisTVBinder)], TcThetaType, TcType)
478 -- (type vars, preds (incl equalities), rho)
479 -- Instantiate the binders of a type signature with TyVarTvs
480 tcInstTypeBndrs id
481 | null tyvars -- There may be overloading despite no type variables;
482 -- (?x :: Int) => Int -> Int
483 = return ([], theta, tau)
484 | otherwise
485 = do { (subst, tyvars') <- mapAccumLM inst_invis_bndr emptyTCvSubst tyvars
486 ; let tv_prs = map (tyVarName . binderVar) tyvars `zip` tyvars'
487 subst' = extendTCvInScopeSet subst (tyCoVarsOfType rho)
488 ; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
489 where
490 (tyvars, rho) = splitForAllInvisTVBinders (idType id)
491 (theta, tau) = tcSplitPhiTy rho
492
493 inst_invis_bndr :: TCvSubst -> InvisTVBinder
494 -> TcM (TCvSubst, InvisTVBinder)
495 inst_invis_bndr subst (Bndr tv spec)
496 = do { (subst', tv') <- newMetaTyVarTyVarX subst tv
497 ; return (subst', Bndr tv' spec) }
498
499 tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
500 -- Instantiate a type signature with skolem constants.
501 -- This freshens the names, but no need to do so
502 tcSkolDFunType dfun
503 = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
504 ; return (map snd tv_prs, theta, tau) }
505
506 tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
507 -- Make skolem constants, but do *not* give them new names, as above
508 -- Moreover, make them "super skolems"; see comments with superSkolemTv
509 -- see Note [Kind substitution when instantiating]
510 -- Precondition: tyvars should be ordered by scoping
511 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
512
513 tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
514 tcSuperSkolTyVar subst tv
515 = (extendTvSubstWithClone subst tv new_tv, new_tv)
516 where
517 kind = substTyUnchecked subst (tyVarKind tv)
518 new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
519
520 -- | Given a list of @['TyVar']@, skolemize the type variables,
521 -- returning a substitution mapping the original tyvars to the
522 -- skolems, and the list of newly bound skolems.
523 tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
524 -- See Note [Skolemising type variables]
525 tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
526
527 tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
528 -- See Note [Skolemising type variables]
529 tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False
530
531 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
532 -- See Note [Skolemising type variables]
533 -- This version freshens the names and creates "super skolems";
534 -- see comments around superSkolemTv.
535 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
536
537 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
538 -- See Note [Skolemising type variables]
539 -- This version freshens the names and creates "super skolems";
540 -- see comments around superSkolemTv.
541 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst
542
543 tcInstSkolTyVarsPushLevel :: Bool -- True <=> make "super skolem"
544 -> TCvSubst -> [TyVar]
545 -> TcM (TCvSubst, [TcTyVar])
546 -- Skolemise one level deeper, hence pushTcLevel
547 -- See Note [Skolemising type variables]
548 tcInstSkolTyVarsPushLevel overlappable subst tvs
549 = do { tc_lvl <- getTcLevel
550 -- Do not retain the whole TcLclEnv
551 ; let !pushed_lvl = pushTcLevel tc_lvl
552 ; tcInstSkolTyVarsAt pushed_lvl overlappable subst tvs }
553
554 tcInstSkolTyVarsAt :: TcLevel -> Bool
555 -> TCvSubst -> [TyVar]
556 -> TcM (TCvSubst, [TcTyVar])
557 tcInstSkolTyVarsAt lvl overlappable subst tvs
558 = freshenTyCoVarsX new_skol_tv subst tvs
559 where
560 details = SkolemTv lvl overlappable
561 new_skol_tv name kind = mkTcTyVar name kind details
562
563 ------------------
564 freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar])
565 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
566 -- as TyVars, rather than becoming TcTyVars
567 -- Used in 'GHC.Tc.Instance.Family.newFamInst', and 'GHC.Tc.Utils.Instantiate.newClsInst'
568 freshenTyVarBndrs = freshenTyCoVars mkTyVar
569
570 freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcM (TCvSubst, [CoVar])
571 -- ^ Give fresh uniques to a bunch of CoVars
572 -- Used in "GHC.Tc.Instance.Family.newFamInst"
573 freshenCoVarBndrsX subst = freshenTyCoVarsX mkCoVar subst
574
575 ------------------
576 freshenTyCoVars :: (Name -> Kind -> TyCoVar)
577 -> [TyVar] -> TcM (TCvSubst, [TyCoVar])
578 freshenTyCoVars mk_tcv = freshenTyCoVarsX mk_tcv emptyTCvSubst
579
580 freshenTyCoVarsX :: (Name -> Kind -> TyCoVar)
581 -> TCvSubst -> [TyCoVar]
582 -> TcM (TCvSubst, [TyCoVar])
583 freshenTyCoVarsX mk_tcv = mapAccumLM (freshenTyCoVarX mk_tcv)
584
585 freshenTyCoVarX :: (Name -> Kind -> TyCoVar)
586 -> TCvSubst -> TyCoVar -> TcM (TCvSubst, TyCoVar)
587 -- This a complete freshening operation:
588 -- the skolems have a fresh unique, and a location from the monad
589 -- See Note [Skolemising type variables]
590 freshenTyCoVarX mk_tcv subst tycovar
591 = do { loc <- getSrcSpanM
592 ; uniq <- newUnique
593 ; let old_name = tyVarName tycovar
594 -- Force so we don't retain reference to the old name and id
595 -- See (#19619) for more discussion
596 !old_occ_name = getOccName old_name
597 new_name = mkInternalName uniq old_occ_name loc
598 new_kind = substTyUnchecked subst (tyVarKind tycovar)
599 new_tcv = mk_tcv new_name new_kind
600 subst1 = extendTCvSubstWithClone subst tycovar new_tcv
601 ; return (subst1, new_tcv) }
602
603 {- Note [Skolemising type variables]
604 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
605 The tcInstSkolTyVars family of functions instantiate a list of TyVars
606 to fresh skolem TcTyVars. Important notes:
607
608 a) Level allocation. We generally skolemise /before/ calling
609 pushLevelAndCaptureConstraints. So we want their level to the level
610 of the soon-to-be-created implication, which has a level ONE HIGHER
611 than the current level. Hence the pushTcLevel. It feels like a
612 slight hack.
613
614 b) The [TyVar] should be ordered (kind vars first)
615 See Note [Kind substitution when instantiating]
616
617 c) Clone the variable to give a fresh unique. This is essential.
618 Consider (tc160)
619 type Foo x = forall a. a -> x
620 And typecheck the expression
621 (e :: Foo (Foo ())
622 We will skolemise the signature, but after expanding synonyms it
623 looks like
624 forall a. a -> forall a. a -> x
625 We don't want to make two big-lambdas with the same unique!
626
627 d) We retain locations. Because the location of the variable is the correct
628 location to report in errors (e.g. in the signature). We don't want the
629 location to change to the body of the function, which does *not* explicitly
630 bind the variable.
631
632 e) The resulting skolems are
633 non-overlappable for tcInstSkolTyVars,
634 but overlappable for tcInstSuperSkolTyVars
635 See GHC.Tc.Deriv.Infer Note [Overlap and deriving] for an example
636 of where this matters.
637
638 Note [Kind substitution when instantiating]
639 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
640 When we instantiate a bunch of kind and type variables, first we
641 expect them to be topologically sorted.
642 Then we have to instantiate the kind variables, build a substitution
643 from old variables to the new variables, then instantiate the type
644 variables substituting the original kind.
645
646 Exemple: If we want to instantiate
647 [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
648 we want
649 [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
650 instead of the bogus
651 [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
652 -}
653
654 {- *********************************************************************
655 * *
656 Literals
657 * *
658 ********************************************************************* -}
659
660 {-
661 In newOverloadedLit we convert directly to an Int or Integer if we
662 know that's what we want. This may save some time, by not
663 temporarily generating overloaded literals, but it won't catch all
664 cases (the rest are caught in lookupInst).
665
666 -}
667
668 newOverloadedLit :: HsOverLit GhcRn
669 -> ExpRhoType
670 -> TcM (HsOverLit GhcTc)
671 newOverloadedLit lit res_ty
672 = do { mb_lit' <- tcShortCutLit lit res_ty
673 ; case mb_lit' of
674 Just lit' -> return lit'
675 Nothing -> newNonTrivialOverloadedLit lit res_ty }
676
677 -- Does not handle things that 'shortCutLit' can handle. See also
678 -- newOverloadedLit in GHC.Tc.Utils.Unify
679 newNonTrivialOverloadedLit :: HsOverLit GhcRn
680 -> ExpRhoType
681 -> TcM (HsOverLit GhcTc)
682 newNonTrivialOverloadedLit
683 lit@(OverLit { ol_val = val, ol_ext = OverLitRn rebindable (L _ meth_name) })
684 res_ty
685 = do { hs_lit <- mkOverLit val
686 ; let lit_ty = hsLitType hs_lit
687 ; (_, fi') <- tcSyntaxOp orig (mkRnSyntaxExpr meth_name)
688 [synKnownType lit_ty] res_ty $
689 \_ _ -> return ()
690 ; let L _ witness = nlHsSyntaxApps fi' [nlHsLit hs_lit]
691 ; res_ty <- readExpType res_ty
692 ; return (lit { ol_ext = OverLitTc { ol_rebindable = rebindable
693 , ol_witness = witness
694 , ol_type = res_ty } }) }
695 where
696 orig = LiteralOrigin lit
697
698 ------------
699 mkOverLit ::OverLitVal -> TcM (HsLit GhcTc)
700 mkOverLit (HsIntegral i)
701 = do { integer_ty <- tcMetaTy integerTyConName
702 ; return (HsInteger (il_text i)
703 (il_value i) integer_ty) }
704
705 mkOverLit (HsFractional r)
706 = do { rat_ty <- tcMetaTy rationalTyConName
707 ; return (HsRat noExtField r rat_ty) }
708
709 mkOverLit (HsIsString src s) = return (HsString src s)
710
711 {-
712 ************************************************************************
713 * *
714 Re-mappable syntax
715
716 Used only for arrow syntax -- find a way to nuke this
717 * *
718 ************************************************************************
719
720 Suppose we are doing the -XRebindableSyntax thing, and we encounter
721 a do-expression. We have to find (>>) in the current environment, which is
722 done by the rename. Then we have to check that it has the same type as
723 Control.Monad.(>>). Or, more precisely, a compatible type. One 'customer' had
724 this:
725
726 (>>) :: HB m n mn => m a -> n b -> mn b
727
728 So the idea is to generate a local binding for (>>), thus:
729
730 let then72 :: forall a b. m a -> m b -> m b
731 then72 = ...something involving the user's (>>)...
732 in
733 ...the do-expression...
734
735 Now the do-expression can proceed using then72, which has exactly
736 the expected type.
737
738 In fact tcSyntaxName just generates the RHS for then72, because we only
739 want an actual binding in the do-expression case. For literals, we can
740 just use the expression inline.
741 -}
742
743 tcSyntaxName :: CtOrigin
744 -> TcType -- ^ Type to instantiate it at
745 -> (Name, HsExpr GhcRn) -- ^ (Standard name, user name)
746 -> TcM (Name, HsExpr GhcTc)
747 -- ^ (Standard name, suitable expression)
748 -- USED ONLY FOR CmdTop (sigh) ***
749 -- See Note [CmdSyntaxTable] in "GHC.Hs.Expr"
750
751 tcSyntaxName orig ty (std_nm, HsVar _ (L _ user_nm))
752 | std_nm == user_nm
753 = do rhs <- newMethodFromName orig std_nm [ty]
754 return (std_nm, rhs)
755
756 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
757 std_id <- tcLookupId std_nm
758 let
759 ([tv], _, tau) = tcSplitSigmaTy (idType std_id)
760 sigma1 = substTyWith [tv] [ty] tau
761 -- Actually, the "tau-type" might be a sigma-type in the
762 -- case of locally-polymorphic methods.
763
764 span <- getSrcSpanM
765 addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1 span) $ do
766
767 -- Check that the user-supplied thing has the
768 -- same type as the standard one.
769 -- Tiresome jiggling because tcCheckSigma takes a located expression
770 expr <- tcCheckPolyExpr (L (noAnnSrcSpan span) user_nm_expr) sigma1
771 hasFixedRuntimeRepRes std_nm user_nm_expr sigma1
772 return (std_nm, unLoc expr)
773
774 syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> SrcSpan -> TidyEnv
775 -> TcRn (TidyEnv, SDoc)
776 syntaxNameCtxt name orig ty loc tidy_env = return (tidy_env, msg)
777 where
778 msg = vcat [ text "When checking that" <+> quotes (ppr name)
779 <+> text "(needed by a syntactic construct)"
780 , nest 2 (text "has the required type:"
781 <+> ppr (tidyType tidy_env ty))
782 , nest 2 (sep [ppr orig, text "at" <+> ppr loc])]
783
784 {-
785 ************************************************************************
786 * *
787 FixedRuntimeRep
788 * *
789 ************************************************************************
790 -}
791
792 -- | Check that the result type of an expression has a fixed runtime representation.
793 --
794 -- Used only for arrow operations such as 'arr', 'first', etc.
795 hasFixedRuntimeRepRes :: Name -> HsExpr GhcRn -> TcSigmaType -> TcM ()
796 hasFixedRuntimeRepRes std_nm user_expr ty = mapM_ do_check mb_arity
797 where
798 do_check :: Arity -> TcM ()
799 do_check arity =
800 let res_ty = nTimes arity (snd . splitPiTy) ty
801 in void $ hasFixedRuntimeRep (FRRArrow $ ArrowFun user_expr) res_ty
802 mb_arity :: Maybe Arity
803 mb_arity -- arity of the arrow operation, counting type-level arguments
804 | std_nm == arrAName -- result used as an argument in, e.g., do_premap
805 = Just 3
806 | std_nm == composeAName -- result used as an argument in, e.g., dsCmdStmt/BodyStmt
807 = Just 5
808 | std_nm == firstAName -- result used as an argument in, e.g., dsCmdStmt/BodyStmt
809 = Just 4
810 | std_nm == appAName -- result used as an argument in, e.g., dsCmd/HsCmdArrApp/HsHigherOrderApp
811 = Just 2
812 | std_nm == choiceAName -- result used as an argument in, e.g., HsCmdIf
813 = Just 5
814 | std_nm == loopAName -- result used as an argument in, e.g., HsCmdIf
815 = Just 4
816 | otherwise
817 = Nothing
818
819 {-
820 ************************************************************************
821 * *
822 Instances
823 * *
824 ************************************************************************
825 -}
826
827 getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
828 -- Construct the OverlapFlag from the global module flags,
829 -- but if the overlap_mode argument is (Just m),
830 -- set the OverlapMode to 'm'
831 getOverlapFlag overlap_mode
832 = do { dflags <- getDynFlags
833 ; let overlap_ok = xopt LangExt.OverlappingInstances dflags
834 incoherent_ok = xopt LangExt.IncoherentInstances dflags
835 use x = OverlapFlag { isSafeOverlap = safeLanguageOn dflags
836 , overlapMode = x }
837 default_oflag | incoherent_ok = use (Incoherent NoSourceText)
838 | overlap_ok = use (Overlaps NoSourceText)
839 | otherwise = use (NoOverlap NoSourceText)
840
841 final_oflag = setOverlapModeMaybe default_oflag overlap_mode
842 ; return final_oflag }
843
844 tcGetInsts :: TcM [ClsInst]
845 -- Gets the local class instances.
846 tcGetInsts = fmap tcg_insts getGblEnv
847
848 newClsInst :: Maybe OverlapMode -> Name -> [TyVar] -> ThetaType
849 -> Class -> [Type] -> TcM ClsInst
850 newClsInst overlap_mode dfun_name tvs theta clas tys
851 = do { (subst, tvs') <- freshenTyVarBndrs tvs
852 -- Be sure to freshen those type variables,
853 -- so they are sure not to appear in any lookup
854 ; let tys' = substTys subst tys
855
856 dfun = mkDictFunId dfun_name tvs theta clas tys
857 -- The dfun uses the original 'tvs' because
858 -- (a) they don't need to be fresh
859 -- (b) they may be mentioned in the ib_binds field of
860 -- an InstInfo, and in GHC.Tc.Utils.Env.pprInstInfoDetails it's
861 -- helpful to use the same names
862
863 ; oflag <- getOverlapFlag overlap_mode
864 ; let inst = mkLocalInstance dfun oflag tvs' clas tys'
865 ; when (isOrphan (is_orphan inst)) $
866 addDiagnostic (TcRnOrphanInstance inst)
867 ; return inst }
868
869 tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
870 -- Add new locally-defined instances
871 tcExtendLocalInstEnv dfuns thing_inside
872 = do { traceDFuns dfuns
873 ; env <- getGblEnv
874 -- Force the access to the TcgEnv so it isn't retained.
875 -- During auditing it is much easier to observe in -hi profiles if
876 -- there are a very small number of TcGblEnv. Keeping a TcGblEnv
877 -- alive is quite dangerous because it contains reference to many
878 -- large data structures.
879 ; let !init_inst_env = tcg_inst_env env
880 !init_insts = tcg_insts env
881 ; (inst_env', cls_insts') <- foldlM addLocalInst
882 (init_inst_env, init_insts)
883 dfuns
884 ; let env' = env { tcg_insts = cls_insts'
885 , tcg_inst_env = inst_env' }
886 ; setGblEnv env' thing_inside }
887
888 addLocalInst :: (InstEnv, [ClsInst]) -> ClsInst -> TcM (InstEnv, [ClsInst])
889 -- Check that the proposed new instance is OK,
890 -- and then add it to the home inst env
891 -- If overwrite_inst, then we can overwrite a direct match
892 addLocalInst (home_ie, my_insts) ispec
893 = do {
894 -- Load imported instances, so that we report
895 -- duplicates correctly
896
897 -- 'matches' are existing instance declarations that are less
898 -- specific than the new one
899 -- 'dups' are those 'matches' that are equal to the new one
900 ; isGHCi <- getIsGHCi
901 ; eps <- getEps
902 ; tcg_env <- getGblEnv
903
904 -- In GHCi, we *override* any identical instances
905 -- that are also defined in the interactive context
906 -- See Note [Override identical instances in GHCi]
907 ; let home_ie'
908 | isGHCi = deleteFromInstEnv home_ie ispec
909 | otherwise = home_ie
910
911 global_ie = eps_inst_env eps
912 inst_envs = InstEnvs { ie_global = global_ie
913 , ie_local = home_ie'
914 , ie_visible = tcVisibleOrphanMods tcg_env }
915
916 -- Check for inconsistent functional dependencies
917 ; let inconsistent_ispecs = checkFunDeps inst_envs ispec
918 ; unless (null inconsistent_ispecs) $
919 funDepErr ispec inconsistent_ispecs
920
921 -- Check for duplicate instance decls.
922 ; let (_tvs, cls, tys) = instanceHead ispec
923 (matches, _, _) = lookupInstEnv False inst_envs cls tys
924 dups = filter (identicalClsInstHead ispec) (map fst matches)
925 ; unless (null dups) $
926 dupInstErr ispec (head dups)
927
928 ; return (extendInstEnv home_ie' ispec, ispec : my_insts) }
929
930 {-
931 Note [Signature files and type class instances]
932 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
933 Instances in signature files do not have an effect when compiling:
934 when you compile a signature against an implementation, you will
935 see the instances WHETHER OR NOT the instance is declared in
936 the file (this is because the signatures go in the EPS and we
937 can't filter them out easily.) This is also why we cannot
938 place the instance in the hi file: it would show up as a duplicate,
939 and we don't have instance reexports anyway.
940
941 However, you might find them useful when typechecking against
942 a signature: the instance is a way of indicating to GHC that
943 some instance exists, in case downstream code uses it.
944
945 Implementing this is a little tricky. Consider the following
946 situation (sigof03):
947
948 module A where
949 instance C T where ...
950
951 module ASig where
952 instance C T
953
954 When compiling ASig, A.hi is loaded, which brings its instances
955 into the EPS. When we process the instance declaration in ASig,
956 we should ignore it for the purpose of doing a duplicate check,
957 since it's not actually a duplicate. But don't skip the check
958 entirely, we still want this to fail (tcfail221):
959
960 module ASig where
961 instance C T
962 instance C T
963
964 Note that in some situations, the interface containing the type
965 class instances may not have been loaded yet at all. The usual
966 situation when A imports another module which provides the
967 instances (sigof02m):
968
969 module A(module B) where
970 import B
971
972 See also Note [Signature lazy interface loading]. We can't
973 rely on this, however, since sometimes we'll have spurious
974 type class instances in the EPS, see #9422 (sigof02dm)
975
976 ************************************************************************
977 * *
978 Errors and tracing
979 * *
980 ************************************************************************
981 -}
982
983 traceDFuns :: [ClsInst] -> TcRn ()
984 traceDFuns ispecs
985 = traceTc "Adding instances:" (vcat (map pp ispecs))
986 where
987 pp ispec = hang (ppr (instanceDFunId ispec) <+> colon)
988 2 (ppr ispec)
989 -- Print the dfun name itself too
990
991 funDepErr :: ClsInst -> [ClsInst] -> TcRn ()
992 funDepErr ispec ispecs
993 = addClsInstsErr TcRnFunDepConflict (ispec NE.:| ispecs)
994
995 dupInstErr :: ClsInst -> ClsInst -> TcRn ()
996 dupInstErr ispec dup_ispec
997 = addClsInstsErr TcRnDupInstanceDecls (ispec NE.:| [dup_ispec])
998
999 addClsInstsErr :: (UnitState -> NE.NonEmpty ClsInst -> TcRnMessage)
1000 -> NE.NonEmpty ClsInst
1001 -> TcRn ()
1002 addClsInstsErr mkErr ispecs = do
1003 unit_state <- hsc_units <$> getTopEnv
1004 setSrcSpan (getSrcSpan (NE.head sorted)) $
1005 addErr $ mkErr unit_state sorted
1006 where
1007 sorted = NE.sortBy (SrcLoc.leftmost_smallest `on` getSrcSpan) ispecs
1008 -- The sortBy just arranges that instances are displayed in order
1009 -- of source location, which reduced wobbling in error messages,
1010 -- and is better for users