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 )
62 import Data.List( mapAccumL )
67 %************************************************************************
71 %************************************************************************
74 emitWanteds :: CtOrigin -> TcThetaType -> TcM [EvVar]
75 emitWanteds origin theta = mapM (emitWanted origin) theta
77 emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
78 emitWanted origin pred = do { loc <- getCtLoc origin
79 ; ev <- newWantedEvVar pred
80 ; emitFlat (mkEvVarX ev loc)
83 newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
84 -- Used when Name is the wired-in name for a wired-in class method,
85 -- so the caller knows its type for sure, which should be of form
86 -- forall a. C a => <blah>
87 -- newMethodFromName is supposed to instantiate just the outer
88 -- type variable and constraint
90 newMethodFromName origin name inst_ty
91 = do { id <- tcLookupId name
92 -- Use tcLookupId not tcLookupGlobalId; the method is almost
93 -- always a class op, but with -XRebindableSyntax GHC is
94 -- meant to find whatever thing is in scope, and that may
95 -- be an ordinary function.
97 ; let (tvs, theta, _caller_knows_this) = tcSplitSigmaTy (idType id)
99 subst = zipOpenTvSubst [the_tv] [inst_ty]
101 ; wrap <- ASSERT( null rest && isSingleton theta )
102 instCall origin [inst_ty] (substTheta subst theta)
103 ; return (mkHsWrap wrap (HsVar id)) }
107 %************************************************************************
109 Deep instantiation and skolemisation
111 %************************************************************************
113 Note [Deep skolemisation]
114 ~~~~~~~~~~~~~~~~~~~~~~~~~
115 deeplySkolemise decomposes and skolemises a type, returning a type
116 with all its arrows visible (ie not buried under foralls)
120 deeplySkolemise (Int -> forall a. Ord a => blah)
121 = ( wp, [a], [d:Ord a], Int -> blah )
122 where wp = \x:Int. /\a. \(d:Ord a). <hole> x
124 deeplySkolemise (forall a. Ord a => Maybe a -> forall b. Eq b => blah)
125 = ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah )
126 where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x
129 if deeplySkolemise ty = (wrap, tvs, evs, rho)
132 and 'wrap' binds tvs, evs
134 ToDo: this eta-abstraction plays fast and loose with termination,
135 because it can introduce extra lambdas. Maybe add a `seq` to
142 -> TcM (HsWrapper, [TyVar], [EvVar], TcRhoType)
145 | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
146 = do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys
147 ; tvs1 <- tcInstSkolTyVars tvs
148 ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs1)
149 ; ev_vars1 <- newEvVars (substTheta subst theta)
150 ; (wrap, tvs2, ev_vars2, rho) <- deeplySkolemise (substTy subst ty')
151 ; return ( mkWpLams ids1
153 <.> mkWpLams ev_vars1
155 <.> mkWpEvVarApps ids1
157 , ev_vars1 ++ ev_vars2
158 , mkFunTys arg_tys rho ) }
161 = return (idHsWrapper, [], [], ty)
163 deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
164 -- Int -> forall a. a -> a ==> (\x:Int. [] x alpha) :: Int -> alpha
166 -- if deeplyInstantiate ty = (wrap, rho)
168 -- then wrap e :: rho
170 deeplyInstantiate orig ty
171 | Just (arg_tys, tvs, theta, rho) <- tcDeepSplitSigmaTy_maybe ty
172 = do { (_, tys, subst) <- tcInstTyVars tvs
173 ; ids1 <- newSysLocalIds (fsLit "di") (substTys subst arg_tys)
174 ; wrap1 <- instCall orig tys (substTheta subst theta)
175 ; (wrap2, rho2) <- deeplyInstantiate orig (substTy subst rho)
176 ; return (mkWpLams ids1
179 <.> mkWpEvVarApps ids1,
180 mkFunTys arg_tys rho2) }
182 | otherwise = return (idHsWrapper, ty)
186 %************************************************************************
190 %************************************************************************
194 instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
195 -- Instantiate the constraints of a call
196 -- (instCall o tys theta)
197 -- (a) Makes fresh dictionaries as necessary for the constraints (theta)
198 -- (b) Throws these dictionaries into the LIE
199 -- (c) Returns an HsWrapper ([.] tys dicts)
201 instCall orig tys theta
202 = do { dict_app <- instCallConstraints orig theta
203 ; return (dict_app <.> mkWpTyApps tys) }
206 instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
207 -- Instantiates the TcTheta, puts all constraints thereby generated
208 -- into the LIE, and returns a HsWrapper to enclose the call site.
210 instCallConstraints _ [] = return idHsWrapper
212 instCallConstraints origin (EqPred ty1 ty2 : preds) -- Try short-cut
213 = do { traceTc "instCallConstraints" $ ppr (EqPred ty1 ty2)
214 ; co <- unifyType ty1 ty2
215 ; co_fn <- instCallConstraints origin preds
216 ; return (co_fn <.> WpEvApp (EvCoercion co)) }
218 instCallConstraints origin (pred : preds)
219 = do { ev_var <- emitWanted origin pred
220 ; co_fn <- instCallConstraints origin preds
221 ; return (co_fn <.> WpEvApp (EvId ev_var)) }
224 instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
225 -- Similar to instCall, but only emit the constraints in the LIE
226 -- Used exclusively for the 'stupid theta' of a data constructor
227 instStupidTheta orig theta
228 = do { _co <- instCallConstraints orig theta -- Discard the coercion
232 %************************************************************************
236 %************************************************************************
238 In newOverloadedLit we convert directly to an Int or Integer if we
239 know that's what we want. This may save some time, by not
240 temporarily generating overloaded literals, but it won't catch all
241 cases (the rest are caught in lookupInst).
244 newOverloadedLit :: CtOrigin
247 -> TcM (HsOverLit TcId)
248 newOverloadedLit orig
249 lit@(OverLit { ol_val = val, ol_rebindable = rebindable
250 , ol_witness = meth_name }) res_ty
253 , Just expr <- shortCutLit val res_ty
254 -- Do not generate a LitInst for rebindable syntax.
255 -- Reason: If we do, tcSimplify will call lookupInst, which
256 -- will call tcSyntaxName, which does unification,
257 -- which tcSimplify doesn't like
258 = return (lit { ol_witness = expr, ol_type = res_ty })
261 = do { hs_lit <- mkOverLit val
262 ; let lit_ty = hsLitType hs_lit
263 ; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
264 -- Overloaded literals must have liftedTypeKind, because
265 -- we're instantiating an overloaded function here,
266 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
267 -- However this'll be picked up by tcSyntaxOp if necessary
268 ; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
269 ; return (lit { ol_witness = witness, ol_type = res_ty }) }
272 mkOverLit :: OverLitVal -> TcM HsLit
273 mkOverLit (HsIntegral i)
274 = do { integer_ty <- tcMetaTy integerTyConName
275 ; return (HsInteger i integer_ty) }
277 mkOverLit (HsFractional r)
278 = do { rat_ty <- tcMetaTy rationalTyConName
279 ; return (HsRat r rat_ty) }
281 mkOverLit (HsIsString s) = return (HsString s)
287 %************************************************************************
291 Used only for arrow syntax -- find a way to nuke this
293 %************************************************************************
295 Suppose we are doing the -XRebindableSyntax thing, and we encounter
296 a do-expression. We have to find (>>) in the current environment, which is
297 done by the rename. Then we have to check that it has the same type as
298 Control.Monad.(>>). Or, more precisely, a compatible type. One 'customer' had
301 (>>) :: HB m n mn => m a -> n b -> mn b
303 So the idea is to generate a local binding for (>>), thus:
305 let then72 :: forall a b. m a -> m b -> m b
306 then72 = ...something involving the user's (>>)...
308 ...the do-expression...
310 Now the do-expression can proceed using then72, which has exactly
313 In fact tcSyntaxName just generates the RHS for then72, because we only
314 want an actual binding in the do-expression case. For literals, we can
315 just use the expression inline.
318 tcSyntaxName :: CtOrigin
319 -> TcType -- Type to instantiate it at
320 -> (Name, HsExpr Name) -- (Standard name, user name)
321 -> TcM (Name, HsExpr TcId) -- (Standard name, suitable expression)
322 -- *** NOW USED ONLY FOR CmdTop (sigh) ***
323 -- NB: tcSyntaxName calls tcExpr, and hence can do unification.
324 -- So we do not call it from lookupInst, which is called from tcSimplify
326 tcSyntaxName orig ty (std_nm, HsVar user_nm)
328 = do rhs <- newMethodFromName orig std_nm ty
331 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
332 std_id <- tcLookupId std_nm
334 -- C.f. newMethodAtLoc
335 ([tv], _, tau) = tcSplitSigmaTy (idType std_id)
336 sigma1 = substTyWith [tv] [ty] tau
337 -- Actually, the "tau-type" might be a sigma-type in the
338 -- case of locally-polymorphic methods.
340 addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
342 -- Check that the user-supplied thing has the
343 -- same type as the standard one.
344 -- Tiresome jiggling because tcCheckSigma takes a located expression
346 expr <- tcPolyExpr (L span user_nm_expr) sigma1
347 return (std_nm, unLoc expr)
349 syntaxNameCtxt :: HsExpr Name -> CtOrigin -> Type -> TidyEnv
350 -> TcRn (TidyEnv, SDoc)
351 syntaxNameCtxt name orig ty tidy_env = do
352 inst_loc <- getCtLoc orig
354 msg = vcat [ptext (sLit "When checking that") <+> quotes (ppr name) <+>
355 ptext (sLit "(needed by a syntactic construct)"),
356 nest 2 (ptext (sLit "has the required type:") <+> ppr (tidyType tidy_env ty)),
357 nest 2 (pprArisingAt inst_loc)]
358 return (tidy_env, msg)
362 %************************************************************************
366 %************************************************************************
369 getOverlapFlag :: TcM OverlapFlag
371 = do { dflags <- getDOpts
372 ; let overlap_ok = xopt Opt_OverlappingInstances dflags
373 incoherent_ok = xopt Opt_IncoherentInstances dflags
374 overlap_flag | incoherent_ok = Incoherent
375 | overlap_ok = OverlapOk
376 | otherwise = NoOverlap
378 ; return overlap_flag }
380 tcGetInstEnvs :: TcM (InstEnv, InstEnv)
381 -- Gets both the external-package inst-env
382 -- and the home-pkg inst env (includes module being compiled)
383 tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
384 return (eps_inst_env eps, tcg_inst_env env) }
386 tcExtendLocalInstEnv :: [Instance] -> TcM a -> TcM a
387 -- Add new locally-defined instances
388 tcExtendLocalInstEnv dfuns thing_inside
389 = do { traceDFuns dfuns
391 ; inst_env' <- foldlM addLocalInst (tcg_inst_env env) dfuns
392 ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
393 tcg_inst_env = inst_env' }
394 ; setGblEnv env' thing_inside }
396 addLocalInst :: InstEnv -> Instance -> TcM InstEnv
397 -- Check that the proposed new instance is OK,
398 -- and then add it to the home inst env
399 addLocalInst home_ie ispec
400 = do { -- Instantiate the dfun type so that we extend the instance
401 -- envt with completely fresh template variables
402 -- This is important because the template variables must
403 -- not overlap with anything in the things being looked up
404 -- (since we do unification).
406 -- We use tcInstSkolType because we don't want to allocate fresh
407 -- *meta* type variables.
409 -- We use UnkSkol --- and *not* InstSkol or PatSkol --- because
410 -- these variables must be bindable by tcUnifyTys. See
411 -- the call to tcUnifyTys in InstEnv, and the special
412 -- treatment that instanceBindFun gives to isOverlappableTyVar
413 -- This is absurdly delicate.
415 let dfun = instanceDFunId ispec
416 ; (tvs', theta', tau') <- tcInstSkolType (idType dfun)
417 ; let (cls, tys') = tcSplitDFunHead tau'
418 dfun' = setIdType dfun (mkSigmaTy tvs' theta' tau')
419 ispec' = setInstanceDFunId ispec dfun'
421 -- Load imported instances, so that we report
422 -- duplicates correctly
424 ; let inst_envs = (eps_inst_env eps, home_ie)
426 -- Check functional dependencies
427 ; case checkFunDeps inst_envs ispec' of
428 Just specs -> funDepErr ispec' specs
431 -- Check for duplicate instance decls
432 ; let { (matches, _) = lookupInstEnv inst_envs cls tys'
433 ; dup_ispecs = [ dup_ispec
434 | (dup_ispec, _) <- matches
435 , let (_,_,_,dup_tys) = instanceHead dup_ispec
436 , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)] }
437 -- Find memebers of the match list which ispec itself matches.
438 -- If the match is 2-way, it's a duplicate
440 dup_ispec : _ -> dupInstErr ispec' dup_ispec
443 -- OK, now extend the envt
444 ; return (extendInstEnv home_ie ispec') }
446 traceDFuns :: [Instance] -> TcRn ()
448 = traceTc "Adding instances:" (vcat (map pp ispecs))
450 pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec
451 -- Print the dfun name itself too
453 funDepErr :: Instance -> [Instance] -> TcRn ()
454 funDepErr ispec ispecs
456 addErr (hang (ptext (sLit "Functional dependencies conflict between instance declarations:"))
457 2 (pprInstances (ispec:ispecs)))
458 dupInstErr :: Instance -> Instance -> TcRn ()
459 dupInstErr ispec dup_ispec
461 addErr (hang (ptext (sLit "Duplicate instance declarations:"))
462 2 (pprInstances [ispec, dup_ispec]))
464 addDictLoc :: Instance -> TcRn a -> TcRn a
465 addDictLoc ispec thing_inside
466 = setSrcSpan (mkSrcSpan loc loc) thing_inside
468 loc = getSrcLoc ispec
471 %************************************************************************
473 Simple functions over evidence variables
475 %************************************************************************
478 unitImplication :: Implication -> Bag Implication
479 unitImplication implic
480 | isEmptyWC (ic_wanted implic) = emptyBag
481 | otherwise = unitBag implic
483 hasEqualities :: [EvVar] -> Bool
484 -- Has a bunch of canonical constraints (all givens) got any equalities in it?
485 hasEqualities givens = any (has_eq . evVarPred) givens
487 has_eq (EqPred {}) = True
488 has_eq (IParam {}) = False
489 has_eq (ClassP cls _tys) = any has_eq (classSCTheta cls)
491 ---------------- Getting free tyvars -------------------------
492 tyVarsOfWC :: WantedConstraints -> TyVarSet
493 tyVarsOfWC (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
494 = tyVarsOfEvVarXs flat `unionVarSet`
495 tyVarsOfBag tyVarsOfImplication implic `unionVarSet`
496 tyVarsOfEvVarXs insol
498 tyVarsOfImplication :: Implication -> TyVarSet
499 tyVarsOfImplication (Implic { ic_skols = skols, ic_wanted = wanted })
500 = tyVarsOfWC wanted `minusVarSet` skols
502 tyVarsOfEvVarX :: EvVarX a -> TyVarSet
503 tyVarsOfEvVarX (EvVarX ev _) = tyVarsOfEvVar ev
505 tyVarsOfEvVarXs :: Bag (EvVarX a) -> TyVarSet
506 tyVarsOfEvVarXs = tyVarsOfBag tyVarsOfEvVarX
508 tyVarsOfEvVar :: EvVar -> TyVarSet
509 tyVarsOfEvVar ev = tyVarsOfPred $ evVarPred ev
511 tyVarsOfEvVars :: [EvVar] -> TyVarSet
512 tyVarsOfEvVars = foldr (unionVarSet . tyVarsOfEvVar) emptyVarSet
514 tyVarsOfBag :: (a -> TyVarSet) -> Bag a -> TyVarSet
515 tyVarsOfBag tvs_of = foldrBag (unionVarSet . tvs_of) emptyVarSet
517 ---------------- Tidying -------------------------
518 tidyWC :: TidyEnv -> WantedConstraints -> WantedConstraints
519 tidyWC env (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
520 = WC { wc_flat = tidyWantedEvVars env flat
521 , wc_impl = mapBag (tidyImplication env) implic
522 , wc_insol = mapBag (tidyFlavoredEvVar env) insol }
524 tidyImplication :: TidyEnv -> Implication -> Implication
525 tidyImplication env implic@(Implic { ic_skols = tvs
529 = implic { ic_skols = mkVarSet tvs'
530 , ic_given = map (tidyEvVar env1) given
531 , ic_wanted = tidyWC env1 wanted
532 , ic_loc = tidyGivenLoc env1 loc }
534 (env1, tvs') = mapAccumL tidyTyVarBndr env (varSetElems tvs)
536 tidyEvVar :: TidyEnv -> EvVar -> EvVar
537 tidyEvVar env var = setVarType var (tidyType env (varType var))
539 tidyWantedEvVar :: TidyEnv -> WantedEvVar -> WantedEvVar
540 tidyWantedEvVar env (EvVarX v l) = EvVarX (tidyEvVar env v) l
542 tidyWantedEvVars :: TidyEnv -> Bag WantedEvVar -> Bag WantedEvVar
543 tidyWantedEvVars env = mapBag (tidyWantedEvVar env)
545 tidyFlavoredEvVar :: TidyEnv -> FlavoredEvVar -> FlavoredEvVar
546 tidyFlavoredEvVar env (EvVarX v fl)
547 = EvVarX (tidyEvVar env v) (tidyFlavor env fl)
549 tidyFlavor :: TidyEnv -> CtFlavor -> CtFlavor
550 tidyFlavor env (Given loc) = Given (tidyGivenLoc env loc)
553 tidyGivenLoc :: TidyEnv -> GivenLoc -> GivenLoc
554 tidyGivenLoc env (CtLoc skol span ctxt) = CtLoc (tidySkolemInfo env skol) span ctxt
556 tidySkolemInfo :: TidyEnv -> SkolemInfo -> SkolemInfo
557 tidySkolemInfo env (SigSkol cx ty) = SigSkol cx (tidyType env ty)
558 tidySkolemInfo env (InferSkol ids) = InferSkol (mapSnd (tidyType env) ids)
559 tidySkolemInfo _ info = info
561 ---------------- Substitution -------------------------
562 substWC :: TvSubst -> WantedConstraints -> WantedConstraints
563 substWC subst (WC { wc_flat = flat, wc_impl = implic, wc_insol = insol })
564 = WC { wc_flat = substWantedEvVars subst flat
565 , wc_impl = mapBag (substImplication subst) implic
566 , wc_insol = mapBag (substFlavoredEvVar subst) insol }
568 substImplication :: TvSubst -> Implication -> Implication
569 substImplication subst implic@(Implic { ic_skols = tvs
573 = implic { ic_skols = mkVarSet tvs'
574 , ic_given = map (substEvVar subst1) given
575 , ic_wanted = substWC subst1 wanted
576 , ic_loc = substGivenLoc subst1 loc }
578 (subst1, tvs') = mapAccumL substTyVarBndr subst (varSetElems tvs)
580 substEvVar :: TvSubst -> EvVar -> EvVar
581 substEvVar subst var = setVarType var (substTy subst (varType var))
583 substWantedEvVars :: TvSubst -> Bag WantedEvVar -> Bag WantedEvVar
584 substWantedEvVars subst = mapBag (substWantedEvVar subst)
586 substWantedEvVar :: TvSubst -> WantedEvVar -> WantedEvVar
587 substWantedEvVar subst (EvVarX v l) = EvVarX (substEvVar subst v) l
589 substFlavoredEvVar :: TvSubst -> FlavoredEvVar -> FlavoredEvVar
590 substFlavoredEvVar subst (EvVarX v fl)
591 = EvVarX (substEvVar subst v) (substFlavor subst fl)
593 substFlavor :: TvSubst -> CtFlavor -> CtFlavor
594 substFlavor subst (Given loc) = Given (substGivenLoc subst loc)
595 substFlavor _ fl = fl
597 substGivenLoc :: TvSubst -> GivenLoc -> GivenLoc
598 substGivenLoc subst (CtLoc skol span ctxt) = CtLoc (substSkolemInfo subst skol) span ctxt
600 substSkolemInfo :: TvSubst -> SkolemInfo -> SkolemInfo
601 substSkolemInfo subst (SigSkol cx ty) = SigSkol cx (substTy subst ty)
602 substSkolemInfo subst (InferSkol ids) = InferSkol (mapSnd (substTy subst) ids)
603 substSkolemInfo _ info = info