2 % (c) The University of Glasgow 2006
3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
6 The @Inst@ type: dictionaries or method instances
11 deeplyInstantiate, instCall, instStupidTheta,
12 emitWanted, emitWanteds,
14 newOverloadedLit, mkOverLit,
16 tcGetInstEnvs, getOverlapFlag, tcExtendLocalInstEnv,
17 instCallConstraints, newMethodFromName,
20 -- Simple functions over evidence variables
21 hasEqualities, unitImplication,
23 tyVarsOfWC, tyVarsOfBag, tyVarsOfEvVarXs, tyVarsOfEvVarX,
24 tyVarsOfEvVar, tyVarsOfEvVars, tyVarsOfImplication,
26 tidyWantedEvVar, tidyWantedEvVars, tidyWC,
27 tidyEvVar, tidyImplication, tidyFlavoredEvVar,
29 substWantedEvVar, substWantedEvVars, substFlavoredEvVar,
30 substEvVar, substImplication
33 #include "HsVersions.h"
35 import {-# SOURCE #-} TcExpr( tcPolyExpr, tcSyntaxOp )
36 import {-# SOURCE #-} TcUnify( unifyType )
52 import Var ( Var, TyVar, EvVar, varType, setVarType )
63 import Data.List( mapAccumL )
68 %************************************************************************
72 %************************************************************************
75 emitWanteds :: CtOrigin -> TcThetaType -> TcM [EvVar]
76 emitWanteds origin theta = mapM (emitWanted origin) theta
78 emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
79 emitWanted origin pred = do { loc <- getCtLoc origin
80 ; ev <- newWantedEvVar pred
81 ; emitFlat (mkEvVarX ev loc)
84 newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
85 -- Used when Name is the wired-in name for a wired-in class method,
86 -- so the caller knows its type for sure, which should be of form
87 -- forall a. C a => <blah>
88 -- newMethodFromName is supposed to instantiate just the outer
89 -- type variable and constraint
91 newMethodFromName origin name inst_ty
92 = do { id <- tcLookupId name
93 -- Use tcLookupId not tcLookupGlobalId; the method is almost
94 -- always a class op, but with -XRebindableSyntax GHC is
95 -- meant to find whatever thing is in scope, and that may
96 -- be an ordinary function.
98 ; let (tvs, theta, _caller_knows_this) = tcSplitSigmaTy (idType id)
100 subst = zipOpenTvSubst [the_tv] [inst_ty]
102 ; wrap <- ASSERT( null rest && isSingleton theta )
103 instCall origin [inst_ty] (substTheta subst theta)
104 ; return (mkHsWrap wrap (HsVar id)) }
108 %************************************************************************
110 Deep instantiation and skolemisation
112 %************************************************************************
114 Note [Deep skolemisation]
115 ~~~~~~~~~~~~~~~~~~~~~~~~~
116 deeplySkolemise decomposes and skolemises a type, returning a type
117 with all its arrows visible (ie not buried under foralls)
121 deeplySkolemise (Int -> forall a. Ord a => blah)
122 = ( wp, [a], [d:Ord a], Int -> blah )
123 where wp = \x:Int. /\a. \(d:Ord a). <hole> x
125 deeplySkolemise (forall a. Ord a => Maybe a -> forall b. Eq b => blah)
126 = ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah )
127 where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x
130 if deeplySkolemise ty = (wrap, tvs, evs, rho)
133 and 'wrap' binds tvs, evs
135 ToDo: this eta-abstraction plays fast and loose with termination,
136 because it can introduce extra lambdas. Maybe add a `seq` to
143 -> TcM (HsWrapper, [TyVar], [EvVar], TcRhoType)
146 | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
147 = do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys
148 ; tvs1 <- tcInstSkolTyVars tvs
149 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs1)
150 ; ev_vars1 <- newEvVars (substTheta subst theta)
151 ; (wrap, tvs2, ev_vars2, rho) <- deeplySkolemise (substTy subst ty')
152 ; return ( mkWpLams ids1
154 <.> mkWpLams ev_vars1
156 <.> mkWpEvVarApps ids1
158 , ev_vars1 ++ ev_vars2
159 , mkFunTys arg_tys rho ) }
162 = return (idHsWrapper, [], [], ty)
164 deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
165 -- Int -> forall a. a -> a ==> (\x:Int. [] x alpha) :: Int -> alpha
167 -- if deeplyInstantiate ty = (wrap, rho)
169 -- then wrap e :: rho
171 deeplyInstantiate orig ty
172 | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
173 = do { (_, tys, subst) <- tcInstTyVars tvs
174 ; ids1 <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
175 ; wrap1 <- instCall orig tys (substTheta subst theta)
176 ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
177 ; return (mkWpLams ids1
180 <.> mkWpEvVarApps ids1,
181 mkFunTys arg_tys rho2) }
183 | otherwise = return (idHsWrapper, ty)
187 %************************************************************************
191 %************************************************************************
195 instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
196 -- Instantiate the constraints of a call
197 -- (instCall o tys theta)
198 -- (a) Makes fresh dictionaries as necessary for the constraints (theta)
199 -- (b) Throws these dictionaries into the LIE
200 -- (c) Returns an HsWrapper ([.] tys dicts)
202 instCall orig tys theta
203 = do { dict_app <- instCallConstraints orig theta
204 ; return (dict_app <.> mkWpTyApps tys) }
207 instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
208 -- Instantiates the TcTheta, puts all constraints thereby generated
209 -- into the LIE, and returns a HsWrapper to enclose the call site.
211 instCallConstraints _ [] = return idHsWrapper
213 instCallConstraints origin (EqPred ty1 ty2 : preds) -- Try short-cut
214 = do { traceTc "instCallConstraints" $ ppr (EqPred ty1 ty2)
215 ; co <- unifyType ty1 ty2
216 ; co_fn <- instCallConstraints origin preds
217 ; return (co_fn <.> WpEvApp (EvCoercion co)) }
219 instCallConstraints origin (pred : preds)
220 = do { ev_var <- emitWanted origin pred
221 ; co_fn <- instCallConstraints origin preds
222 ; return (co_fn <.> WpEvApp (EvId ev_var)) }
225 instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
226 -- Similar to instCall, but only emit the constraints in the LIE
227 -- Used exclusively for the 'stupid theta' of a data constructor
228 instStupidTheta orig theta
229 = do { _co <- instCallConstraints orig theta -- Discard the coercion
233 %************************************************************************
237 %************************************************************************
239 In newOverloadedLit we convert directly to an Int or Integer if we
240 know that's what we want. This may save some time, by not
241 temporarily generating overloaded literals, but it won't catch all
242 cases (the rest are caught in lookupInst).
245 newOverloadedLit :: CtOrigin
248 -> TcM (HsOverLit TcId)
249 newOverloadedLit orig
250 lit@(OverLit { ol_val = val, ol_rebindable = rebindable
251 , ol_witness = meth_name }) res_ty
254 , Just expr <- shortCutLit val res_ty
255 -- Do not generate a LitInst for rebindable syntax.
256 -- Reason: If we do, tcSimplify will call lookupInst, which
257 -- will call tcSyntaxName, which does unification,
258 -- which tcSimplify doesn't like
259 = return (lit { ol_witness = expr, ol_type = res_ty })
262 = do { hs_lit <- mkOverLit val
263 ; let lit_ty = hsLitType hs_lit
264 ; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
265 -- Overloaded literals must have liftedTypeKind, because
266 -- we're instantiating an overloaded function here,
267 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
268 -- However this'll be picked up by tcSyntaxOp if necessary
269 ; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
270 ; return (lit { ol_witness = witness, ol_type = res_ty }) }
273 mkOverLit :: OverLitVal -> TcM HsLit
274 mkOverLit (HsIntegral i)
275 = do { integer_ty <- tcMetaTy integerTyConName
276 ; return (HsInteger i integer_ty) }
278 mkOverLit (HsFractional r)
279 = do { rat_ty <- tcMetaTy rationalTyConName
280 ; return (HsRat (fl_value r) rat_ty) }
282 mkOverLit (HsIsString s) = return (HsString s)
288 %************************************************************************
292 Used only for arrow syntax -- find a way to nuke this
294 %************************************************************************
296 Suppose we are doing the -XRebindableSyntax thing, and we encounter
297 a do-expression. We have to find (>>) in the current environment, which is
298 done by the rename. Then we have to check that it has the same type as
299 Control.Monad.(>>). Or, more precisely, a compatible type. One 'customer' had
302 (>>) :: HB m n mn => m a -> n b -> mn b
304 So the idea is to generate a local binding for (>>), thus:
306 let then72 :: forall a b. m a -> m b -> m b
307 then72 = ...something involving the user's (>>)...
309 ...the do-expression...
311 Now the do-expression can proceed using then72, which has exactly
314 In fact tcSyntaxName just generates the RHS for then72, because we only
315 want an actual binding in the do-expression case. For literals, we can
316 just use the expression inline.
319 tcSyntaxName :: CtOrigin
320 -> TcType -- Type to instantiate it at
321 -> (Name, HsExpr Name) -- (Standard name, user name)
322 -> TcM (Name, HsExpr TcId) -- (Standard name, suitable expression)
323 -- *** NOW USED ONLY FOR CmdTop (sigh) ***
324 -- NB: tcSyntaxName calls tcExpr, and hence can do unification.
325 -- So we do not call it from lookupInst, which is called from tcSimplify
327 tcSyntaxName orig ty (std_nm, HsVar user_nm)
329 = do rhs <- newMethodFromName orig std_nm ty
332 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
333 std_id <- tcLookupId std_nm
335 -- C.f. newMethodAtLoc
336 ([tv], _, tau) = tcSplitSigmaTy (idType std_id)
337 sigma1 = substTyWith [tv] [ty] tau
338 -- Actually, the "tau-type" might be a sigma-type in the
339 -- case of locally-polymorphic methods.
341 addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
343 -- Check that the user-supplied thing has the
344 -- same type as the standard one.
345 -- Tiresome jiggling because tcCheckSigma takes a located expression
347 expr <- tcPolyExpr (L span user_nm_expr) sigma1
348 return (std_nm, unLoc expr)
350 syntaxNameCtxt :: HsExpr Name -> CtOrigin -> Type -> TidyEnv
351 -> TcRn (TidyEnv, SDoc)
352 syntaxNameCtxt name orig ty tidy_env = do
353 inst_loc <- getCtLoc orig
355 msg = vcat [ptext (sLit "When checking that") <+> quotes (ppr name) <+>
356 ptext (sLit "(needed by a syntactic construct)"),
357 nest 2 (ptext (sLit "has the required type:") <+> ppr (tidyType tidy_env ty)),
358 nest 2 (pprArisingAt inst_loc)]
359 return (tidy_env, msg)
363 %************************************************************************
367 %************************************************************************
370 getOverlapFlag :: TcM OverlapFlag
372 = do { dflags <- getDOpts
373 ; let overlap_ok = xopt Opt_OverlappingInstances dflags
374 incoherent_ok = xopt Opt_IncoherentInstances dflags
375 overlap_flag | incoherent_ok = Incoherent
376 | overlap_ok = OverlapOk
377 | otherwise = NoOverlap
379 ; return overlap_flag }
381 tcGetInstEnvs :: TcM (InstEnv, InstEnv)
382 -- Gets both the external-package inst-env
383 -- and the home-pkg inst env (includes module being compiled)
384 tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
385 return (eps_inst_env eps, tcg_inst_env env) }
387 tcExtendLocalInstEnv :: [Instance] -> TcM a -> TcM a
388 -- Add new locally-defined instances
389 tcExtendLocalInstEnv dfuns thing_inside
390 = do { traceDFuns dfuns
392 ; inst_env' <- foldlM addLocalInst (tcg_inst_env env) dfuns
393 ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
394 tcg_inst_env = inst_env' }
395 ; setGblEnv env' thing_inside }
397 addLocalInst :: InstEnv -> Instance -> TcM InstEnv
398 -- Check that the proposed new instance is OK,
399 -- and then add it to the home inst env
400 addLocalInst home_ie ispec
401 = do { -- Instantiate the dfun type so that we extend the instance
402 -- envt with completely fresh template variables
403 -- This is important because the template variables must
404 -- not overlap with anything in the things being looked up
405 -- (since we do unification).
407 -- We use tcInstSkolType because we don't want to allocate fresh
408 -- *meta* type variables.
410 -- We use UnkSkol --- and *not* InstSkol or PatSkol --- because
411 -- these variables must be bindable by tcUnifyTys. See
412 -- the call to tcUnifyTys in InstEnv, and the special
413 -- treatment that instanceBindFun gives to isOverlappableTyVar
414 -- This is absurdly delicate.
416 let dfun = instanceDFunId ispec
417 ; (tvs', theta', tau') <- tcInstSkolType (idType dfun)
418 ; let (cls, tys') = tcSplitDFunHead tau'
419 dfun' = setIdType dfun (mkSigmaTy tvs' theta' tau')
420 ispec' = setInstanceDFunId ispec dfun'
422 -- Load imported instances, so that we report
423 -- duplicates correctly
425 ; let inst_envs = (eps_inst_env eps, home_ie)
427 -- Check functional dependencies
428 ; case checkFunDeps inst_envs ispec' of
429 Just specs -> funDepErr ispec' specs
432 -- Check for duplicate instance decls
433 ; let { (matches, _) = lookupInstEnv inst_envs cls tys'
434 ; dup_ispecs = [ dup_ispec
435 | (dup_ispec, _) <- matches
436 , let (_,_,_,dup_tys) = instanceHead dup_ispec
437 , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)] }
438 -- Find memebers of the match list which ispec itself matches.
439 -- If the match is 2-way, it's a duplicate
441 dup_ispec : _ -> dupInstErr ispec' dup_ispec
444 -- OK, now extend the envt
445 ; return (extendInstEnv home_ie ispec') }
447 traceDFuns :: [Instance] -> TcRn ()
449 = traceTc "Adding instances:" (vcat (map pp ispecs))
451 pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec
452 -- Print the dfun name itself too
454 funDepErr :: Instance -> [Instance] -> TcRn ()
455 funDepErr ispec ispecs
457 addErr (hang (ptext (sLit "Functional dependencies conflict between instance declarations:"))
458 2 (pprInstances (ispec:ispecs)))
459 dupInstErr :: Instance -> Instance -> TcRn ()
460 dupInstErr ispec dup_ispec
462 addErr (hang (ptext (sLit "Duplicate instance declarations:"))
463 2 (pprInstances [ispec, dup_ispec]))
465 addDictLoc :: Instance -> TcRn a -> TcRn a
466 addDictLoc ispec thing_inside
467 = setSrcSpan (mkSrcSpan loc loc) thing_inside
469 loc = getSrcLoc ispec
472 %************************************************************************
474 Simple functions over evidence variables
476 %************************************************************************
479 unitImplication :: Implication -> Bag Implication
480 unitImplication implic
481 | isEmptyWC (ic_wanted implic) = emptyBag
482 | otherwise = unitBag implic
484 hasEqualities :: [EvVar] -> Bool
485 -- Has a bunch of canonical constraints (all givens) got any equalities in it?
486 hasEqualities givens = any (has_eq . evVarPred) givens
488 has_eq (EqPred {}) = True
489 has_eq (IParam {}) = False
490 has_eq (ClassP cls _tys) = any has_eq (classSCTheta cls)
492 ---------------- Getting free tyvars -------------------------
493 tyVarsOfWC :: WantedConstraints -> TyVarSet
494 tyVarsOfWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
495 = tyVarsOfEvVarXs flat `unionVarSet`
496 tyVarsOfBag tyVarsOfImplication implic `unionVarSet`
497 tyVarsOfEvVarXs insol
499 tyVarsOfImplication :: Implication -> TyVarSet
500 tyVarsOfImplication (Implic { ic_skols = skols, ic_wanted = wanted })
501 = tyVarsOfWC wanted `minusVarSet` skols
503 tyVarsOfEvVarX :: EvVarX a -> TyVarSet
504 tyVarsOfEvVarX (EvVarX ev _) = tyVarsOfEvVar ev
506 tyVarsOfEvVarXs :: Bag (EvVarX a) -> TyVarSet
507 tyVarsOfEvVarXs = tyVarsOfBag tyVarsOfEvVarX
509 tyVarsOfEvVar :: EvVar -> TyVarSet
510 tyVarsOfEvVar ev = tyVarsOfPred $ evVarPred ev
512 tyVarsOfEvVars :: [EvVar] -> TyVarSet
513 tyVarsOfEvVars = foldr (unionVarSet . tyVarsOfEvVar) emptyVarSet
515 tyVarsOfBag :: (a -> TyVarSet) -> Bag a -> TyVarSet
516 tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
518 ---------------- Tidying -------------------------
519 tidyWC :: TidyEnv -> WantedConstraints -> WantedConstraints
520 tidyWC env (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
521 = WC { wc_flat = tidyWantedEvVars env flat
522 , wc_impl = mapBag (tidyImplication env) implic
523 , wc_insol = mapBag (tidyFlavoredEvVar env) insol }
525 tidyImplication :: TidyEnv -> Implication -> Implication
526 tidyImplication env implic@(Implic { ic_skols = tvs
530 = implic { ic_skols = mkVarSet tvs'
531 , ic_given = map (tidyEvVar env1) given
532 , ic_wanted = tidyWC env1 wanted
533 , ic_loc = tidyGivenLoc env1 loc }
535 (env1, tvs') = mapAccumL tidyTyVarBndr env (varSetElems tvs)
537 tidyEvVar :: TidyEnv -> EvVar -> EvVar
538 tidyEvVar env var = setVarType var (tidyType env (varType var))
540 tidyWantedEvVar :: TidyEnv -> WantedEvVar -> WantedEvVar
541 tidyWantedEvVar env (EvVarX v l) = EvVarX (tidyEvVar env v) l
543 tidyWantedEvVars :: TidyEnv -> Bag WantedEvVar -> Bag WantedEvVar
544 tidyWantedEvVars env = mapBag (tidyWantedEvVar env)
546 tidyFlavoredEvVar :: TidyEnv -> FlavoredEvVar -> FlavoredEvVar
547 tidyFlavoredEvVar env (EvVarX v fl)
548 = EvVarX (tidyEvVar env v) (tidyFlavor env fl)
550 tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor
551 tidyFlavor env (Given loc) = Given (tidyGivenLoc env loc)
554 tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
555 tidyGivenLoc env (CtLoc skol span ctxt) = CtLoc (tidySkolemInfo env skol) span ctxt
557 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
558 tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
559 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
560 tidySkolemInfo _ info = info
562 ---------------- Substitution -------------------------
563 substWC :: TvSubst -> WantedConstraints -> WantedConstraints
564 substWC subst (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
565 = WC { wc_flat = substWantedEvVars subst flat
566 , wc_impl = mapBag (substImplication subst) implic
567 , wc_insol = mapBag (substFlavoredEvVar subst) insol }
569 substImplication :: TvSubst -> Implication -> Implication
570 substImplication subst implic@(Implic { ic_skols = tvs
574 = implic { ic_skols = mkVarSet tvs'
575 , ic_given = map (substEvVar subst1) given
576 , ic_wanted = substWC subst1 wanted
577 , ic_loc = substGivenLoc subst1 loc }
579 (subst1, tvs') = mapAccumL substTyVarBndr subst (varSetElems tvs)
581 substEvVar :: TvSubst -> EvVar -> EvVar
582 substEvVar subst var = setVarType var (substTy subst (varType var))
584 substWantedEvVars :: TvSubst -> Bag WantedEvVar -> Bag WantedEvVar
585 substWantedEvVars subst = mapBag (substWantedEvVar subst)
587 substWantedEvVar :: TvSubst -> WantedEvVar -> WantedEvVar
588 substWantedEvVar subst (EvVarX v l) = EvVarX (substEvVar subst v) l
590 substFlavoredEvVar :: TvSubst -> FlavoredEvVar -> FlavoredEvVar
591 substFlavoredEvVar subst (EvVarX v fl)
592 = EvVarX (substEvVar subst v) (substFlavor subst fl)
594 substFlavor :: TvSubst -> CtFlavor -> CtFlavor
595 substFlavor subst (Given loc) = Given (substGivenLoc subst loc)
596 substFlavor _ fl = fl
598 substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
599 substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt
601 substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo
602 substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
603 substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids)
604 substSkolemInfo _ info = info