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 )
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 ; coi <- unifyType ty1 ty2
216 ; co_fn <- instCallConstraints origin preds
217 ; let co = case coi of
220 ; return (co_fn <.> WpEvApp (EvCoercion co)) }
222 instCallConstraints origin (pred : preds)
223 = do { ev_var <- emitWanted origin pred
224 ; co_fn <- instCallConstraints origin preds
225 ; return (co_fn <.> WpEvApp (EvId ev_var)) }
228 instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
229 -- Similar to instCall, but only emit the constraints in the LIE
230 -- Used exclusively for the 'stupid theta' of a data constructor
231 instStupidTheta orig theta
232 = do { _co <- instCallConstraints orig theta -- Discard the coercion
236 %************************************************************************
240 %************************************************************************
242 In newOverloadedLit we convert directly to an Int or Integer if we
243 know that's what we want. This may save some time, by not
244 temporarily generating overloaded literals, but it won't catch all
245 cases (the rest are caught in lookupInst).
248 newOverloadedLit :: CtOrigin
251 -> TcM (HsOverLit TcId)
252 newOverloadedLit orig
253 lit@(OverLit { ol_val = val, ol_rebindable = rebindable
254 , ol_witness = meth_name }) res_ty
257 , Just expr <- shortCutLit val res_ty
258 -- Do not generate a LitInst for rebindable syntax.
259 -- Reason: If we do, tcSimplify will call lookupInst, which
260 -- will call tcSyntaxName, which does unification,
261 -- which tcSimplify doesn't like
262 = return (lit { ol_witness = expr, ol_type = res_ty })
265 = do { hs_lit <- mkOverLit val
266 ; let lit_ty = hsLitType hs_lit
267 ; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
268 -- Overloaded literals must have liftedTypeKind, because
269 -- we're instantiating an overloaded function here,
270 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
271 -- However this'll be picked up by tcSyntaxOp if necessary
272 ; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
273 ; return (lit { ol_witness = witness, ol_type = res_ty }) }
276 mkOverLit :: OverLitVal -> TcM HsLit
277 mkOverLit (HsIntegral i)
278 = do { integer_ty <- tcMetaTy integerTyConName
279 ; return (HsInteger i integer_ty) }
281 mkOverLit (HsFractional r)
282 = do { rat_ty <- tcMetaTy rationalTyConName
283 ; return (HsRat r rat_ty) }
285 mkOverLit (HsIsString s) = return (HsString s)
291 %************************************************************************
295 Used only for arrow syntax -- find a way to nuke this
297 %************************************************************************
299 Suppose we are doing the -XRebindableSyntax thing, and we encounter
300 a do-expression. We have to find (>>) in the current environment, which is
301 done by the rename. Then we have to check that it has the same type as
302 Control.Monad.(>>). Or, more precisely, a compatible type. One 'customer' had
305 (>>) :: HB m n mn => m a -> n b -> mn b
307 So the idea is to generate a local binding for (>>), thus:
309 let then72 :: forall a b. m a -> m b -> m b
310 then72 = ...something involving the user's (>>)...
312 ...the do-expression...
314 Now the do-expression can proceed using then72, which has exactly
317 In fact tcSyntaxName just generates the RHS for then72, because we only
318 want an actual binding in the do-expression case. For literals, we can
319 just use the expression inline.
322 tcSyntaxName :: CtOrigin
323 -> TcType -- Type to instantiate it at
324 -> (Name, HsExpr Name) -- (Standard name, user name)
325 -> TcM (Name, HsExpr TcId) -- (Standard name, suitable expression)
326 -- *** NOW USED ONLY FOR CmdTop (sigh) ***
327 -- NB: tcSyntaxName calls tcExpr, and hence can do unification.
328 -- So we do not call it from lookupInst, which is called from tcSimplify
330 tcSyntaxName orig ty (std_nm, HsVar user_nm)
332 = do rhs <- newMethodFromName orig std_nm ty
335 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
336 std_id <- tcLookupId std_nm
338 -- C.f. newMethodAtLoc
339 ([tv], _, tau) = tcSplitSigmaTy (idType std_id)
340 sigma1 = substTyWith [tv] [ty] tau
341 -- Actually, the "tau-type" might be a sigma-type in the
342 -- case of locally-polymorphic methods.
344 addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
346 -- Check that the user-supplied thing has the
347 -- same type as the standard one.
348 -- Tiresome jiggling because tcCheckSigma takes a located expression
350 expr <- tcPolyExpr (L span user_nm_expr) sigma1
351 return (std_nm, unLoc expr)
353 syntaxNameCtxt :: HsExpr Name -> CtOrigin -> Type -> TidyEnv
354 -> TcRn (TidyEnv, SDoc)
355 syntaxNameCtxt name orig ty tidy_env = do
356 inst_loc <- getCtLoc orig
358 msg = vcat [ptext (sLit "When checking that") <+> quotes (ppr name) <+>
359 ptext (sLit "(needed by a syntactic construct)"),
360 nest 2 (ptext (sLit "has the required type:") <+> ppr (tidyType tidy_env ty)),
361 nest 2 (pprArisingAt inst_loc)]
362 return (tidy_env, msg)
366 %************************************************************************
370 %************************************************************************
373 getOverlapFlag :: TcM OverlapFlag
375 = do { dflags <- getDOpts
376 ; let overlap_ok = xopt Opt_OverlappingInstances dflags
377 incoherent_ok = xopt Opt_IncoherentInstances dflags
378 overlap_flag | incoherent_ok = Incoherent
379 | overlap_ok = OverlapOk
380 | otherwise = NoOverlap
382 ; return overlap_flag }
384 tcGetInstEnvs :: TcM (InstEnv, InstEnv)
385 -- Gets both the external-package inst-env
386 -- and the home-pkg inst env (includes module being compiled)
387 tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
388 return (eps_inst_env eps, tcg_inst_env env) }
390 tcExtendLocalInstEnv :: [Instance] -> TcM a -> TcM a
391 -- Add new locally-defined instances
392 tcExtendLocalInstEnv dfuns thing_inside
393 = do { traceDFuns dfuns
395 ; inst_env' <- foldlM addLocalInst (tcg_inst_env env) dfuns
396 ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
397 tcg_inst_env = inst_env' }
398 ; setGblEnv env' thing_inside }
400 addLocalInst :: InstEnv -> Instance -> TcM InstEnv
401 -- Check that the proposed new instance is OK,
402 -- and then add it to the home inst env
403 addLocalInst home_ie ispec
404 = do { -- Instantiate the dfun type so that we extend the instance
405 -- envt with completely fresh template variables
406 -- This is important because the template variables must
407 -- not overlap with anything in the things being looked up
408 -- (since we do unification).
410 -- We use tcInstSkolType because we don't want to allocate fresh
411 -- *meta* type variables.
413 -- We use UnkSkol --- and *not* InstSkol or PatSkol --- because
414 -- these variables must be bindable by tcUnifyTys. See
415 -- the call to tcUnifyTys in InstEnv, and the special
416 -- treatment that instanceBindFun gives to isOverlappableTyVar
417 -- This is absurdly delicate.
419 let dfun = instanceDFunId ispec
420 ; (tvs', theta', tau') <- tcInstSkolType (idType dfun)
421 ; let (cls, tys') = tcSplitDFunHead tau'
422 dfun' = setIdType dfun (mkSigmaTy tvs' theta' tau')
423 ispec' = setInstanceDFunId ispec dfun'
425 -- Load imported instances, so that we report
426 -- duplicates correctly
428 ; let inst_envs = (eps_inst_env eps, home_ie)
430 -- Check functional dependencies
431 ; case checkFunDeps inst_envs ispec' of
432 Just specs -> funDepErr ispec' specs
435 -- Check for duplicate instance decls
436 ; let { (matches, _) = lookupInstEnv inst_envs cls tys'
437 ; dup_ispecs = [ dup_ispec
438 | (dup_ispec, _) <- matches
439 , let (_,_,_,dup_tys) = instanceHead dup_ispec
440 , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)] }
441 -- Find memebers of the match list which ispec itself matches.
442 -- If the match is 2-way, it's a duplicate
444 dup_ispec : _ -> dupInstErr ispec' dup_ispec
447 -- OK, now extend the envt
448 ; return (extendInstEnv home_ie ispec') }
450 traceDFuns :: [Instance] -> TcRn ()
452 = traceTc "Adding instances:" (vcat (map pp ispecs))
454 pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec
455 -- Print the dfun name itself too
457 funDepErr :: Instance -> [Instance] -> TcRn ()
458 funDepErr ispec ispecs
460 addErr (hang (ptext (sLit "Functional dependencies conflict between instance declarations:"))
461 2 (pprInstances (ispec:ispecs)))
462 dupInstErr :: Instance -> Instance -> TcRn ()
463 dupInstErr ispec dup_ispec
465 addErr (hang (ptext (sLit "Duplicate instance declarations:"))
466 2 (pprInstances [ispec, dup_ispec]))
468 addDictLoc :: Instance -> TcRn a -> TcRn a
469 addDictLoc ispec thing_inside
470 = setSrcSpan (mkSrcSpan loc loc) thing_inside
472 loc = getSrcLoc ispec
475 %************************************************************************
477 Simple functions over evidence variables
479 %************************************************************************
482 unitImplication :: Implication -> Bag Implication
483 unitImplication implic
484 | isEmptyWC (ic_wanted implic) = emptyBag
485 | otherwise = unitBag implic
487 hasEqualities :: [EvVar] -> Bool
488 -- Has a bunch of canonical constraints (all givens) got any equalities in it?
489 hasEqualities givens = any (has_eq . evVarPred) givens
491 has_eq (EqPred {}) = True
492 has_eq (IParam {}) = False
493 has_eq (ClassP cls _tys) = any has_eq (classSCTheta cls)
495 ---------------- Getting free tyvars -------------------------
496 tyVarsOfWC :: WantedConstraints -> TyVarSet
497 tyVarsOfWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
498 = tyVarsOfEvVarXs flat `unionVarSet`
499 tyVarsOfBag tyVarsOfImplication implic `unionVarSet`
500 tyVarsOfEvVarXs insol
502 tyVarsOfImplication :: Implication -> TyVarSet
503 tyVarsOfImplication (Implic { ic_skols = skols, ic_wanted = wanted })
504 = tyVarsOfWC wanted `minusVarSet` skols
506 tyVarsOfEvVarX :: EvVarX a -> TyVarSet
507 tyVarsOfEvVarX (EvVarX ev _) = tyVarsOfEvVar ev
509 tyVarsOfEvVarXs :: Bag (EvVarX a) -> TyVarSet
510 tyVarsOfEvVarXs = tyVarsOfBag tyVarsOfEvVarX
512 tyVarsOfEvVar :: EvVar -> TyVarSet
513 tyVarsOfEvVar ev = tyVarsOfPred $ evVarPred ev
515 tyVarsOfEvVars :: [EvVar] -> TyVarSet
516 tyVarsOfEvVars = foldr (unionVarSet . tyVarsOfEvVar) emptyVarSet
518 tyVarsOfBag :: (a -> TyVarSet) -> Bag a -> TyVarSet
519 tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
521 ---------------- Tidying -------------------------
522 tidyWC :: TidyEnv -> WantedConstraints -> WantedConstraints
523 tidyWC env (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
524 = WC { wc_flat = tidyWantedEvVars env flat
525 , wc_impl = mapBag (tidyImplication env) implic
526 , wc_insol = mapBag (tidyFlavoredEvVar env) insol }
528 tidyImplication :: TidyEnv -> Implication -> Implication
529 tidyImplication env implic@(Implic { ic_skols = tvs
533 = implic { ic_skols = mkVarSet tvs'
534 , ic_given = map (tidyEvVar env1) given
535 , ic_wanted = tidyWC env1 wanted
536 , ic_loc = tidyGivenLoc env1 loc }
538 (env1, tvs') = mapAccumL tidyTyVarBndr env (varSetElems tvs)
540 tidyEvVar :: TidyEnv -> EvVar -> EvVar
541 tidyEvVar env var = setVarType var (tidyType env (varType var))
543 tidyWantedEvVar :: TidyEnv -> WantedEvVar -> WantedEvVar
544 tidyWantedEvVar env (EvVarX v l) = EvVarX (tidyEvVar env v) l
546 tidyWantedEvVars :: TidyEnv -> Bag WantedEvVar -> Bag WantedEvVar
547 tidyWantedEvVars env = mapBag (tidyWantedEvVar env)
549 tidyFlavoredEvVar :: TidyEnv -> FlavoredEvVar -> FlavoredEvVar
550 tidyFlavoredEvVar env (EvVarX v fl)
551 = EvVarX (tidyEvVar env v) (tidyFlavor env fl)
553 tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor
554 tidyFlavor env (Given loc) = Given (tidyGivenLoc env loc)
557 tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
558 tidyGivenLoc env (CtLoc skol span ctxt) = CtLoc (tidySkolemInfo env skol) span ctxt
560 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
561 tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
562 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
563 tidySkolemInfo _ info = info
565 ---------------- Substitution -------------------------
566 substWC :: TvSubst -> WantedConstraints -> WantedConstraints
567 substWC subst (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
568 = WC { wc_flat = substWantedEvVars subst flat
569 , wc_impl = mapBag (substImplication subst) implic
570 , wc_insol = mapBag (substFlavoredEvVar subst) insol }
572 substImplication :: TvSubst -> Implication -> Implication
573 substImplication subst implic@(Implic { ic_skols = tvs
577 = implic { ic_skols = mkVarSet tvs'
578 , ic_given = map (substEvVar subst1) given
579 , ic_wanted = substWC subst1 wanted
580 , ic_loc = substGivenLoc subst1 loc }
582 (subst1, tvs') = mapAccumL substTyVarBndr subst (varSetElems tvs)
584 substEvVar :: TvSubst -> EvVar -> EvVar
585 substEvVar subst var = setVarType var (substTy subst (varType var))
587 substWantedEvVars :: TvSubst -> Bag WantedEvVar -> Bag WantedEvVar
588 substWantedEvVars subst = mapBag (substWantedEvVar subst)
590 substWantedEvVar :: TvSubst -> WantedEvVar -> WantedEvVar
591 substWantedEvVar subst (EvVarX v l) = EvVarX (substEvVar subst v) l
593 substFlavoredEvVar :: TvSubst -> FlavoredEvVar -> FlavoredEvVar
594 substFlavoredEvVar subst (EvVarX v fl)
595 = EvVarX (substEvVar subst v) (substFlavor subst fl)
597 substFlavor :: TvSubst -> CtFlavor -> CtFlavor
598 substFlavor subst (Given loc) = Given (substGivenLoc subst loc)
599 substFlavor _ fl = fl
601 substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
602 substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt
604 substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo
605 substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
606 substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids)
607 substSkolemInfo _ info = info