compiler/typecheck/Inst.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   4 %
   5
   6 The @Inst@ type: dictionaries or method instances
   7
   8 \begin{code}
   9 module Inst (
  10        deeplySkolemise,
  11        deeplyInstantiate, instCall, instStupidTheta,
  12        emitWanted, emitWanteds,
  13
  14        newOverloadedLit, mkOverLit,
  15
  16        tcGetInstEnvs, getOverlapFlag, tcExtendLocalInstEnv,
  17        instCallConstraints, newMethodFromName,
  18        tcSyntaxName,
  19
  20        -- Simple functions over evidence variables
  21        hasEqualities,
  22
  23        tyVarsOfWanteds, tyVarsOfWanted, tyVarsOfWantedEvVar, tyVarsOfWantedEvVars,
  24        tyVarsOfEvVar, tyVarsOfEvVars, tyVarsOfImplication,
  25        tidyWanteds, tidyWanted, tidyWantedEvVar, tidyWantedEvVars,
  26        tidyEvVar, tidyImplication
  27
  28     ) where
  29
  30 #include "HsVersions.h"
  31
  32 import {-# SOURCE #-}   TcExpr( tcPolyExpr, tcSyntaxOp )
  33 import {-# SOURCE #-}   TcUnify( unifyType )
  34
  35 import FastString
  36 import HsSyn
  37 import TcHsSyn
  38 import TcRnMonad
  39 import TcEnv
  40 import TcRnTypes
  41 import InstEnv
  42 import FunDeps
  43 import TcMType
  44 import TcType
  45 import Class
  46 import Unify
  47 import Coercion
  48 import HscTypes
  49 import Id
  50 import Name
  51 import Var      ( Var, TyVar, EvVar, varType, setVarType )
  52 import VarEnv
  53 import VarSet
  54 import PrelNames
  55 import SrcLoc
  56 import DynFlags
  57 import Bag
  58 import Maybes
  59 import Util
  60 import Outputable
  61 import Data.List
  62 \end{code}
  63
  64
  65
  66 %************************************************************************
  67 %*                                                                      *
  68                 Emitting constraints
  69 %*                                                                      *
  70 %************************************************************************
  71
  72 \begin{code}
  73 emitWanteds :: CtOrigin -> TcThetaType -> TcM [EvVar]
  74 emitWanteds origin theta = mapM (emitWanted origin) theta
  75
  76 emitWanted :: CtOrigin -> TcPredType -> TcM EvVar
  77 emitWanted origin pred = do { loc <- getCtLoc origin
  78                             ; ev  <- newWantedEvVar pred
  79                             ; emitConstraint (WcEvVar (WantedEvVar ev loc))
  80                             ; return ev }
  81
  82 newMethodFromName :: CtOrigin -> Name -> TcRhoType -> TcM (HsExpr TcId)
  83 -- Used when Name is the wired-in name for a wired-in class method,
  84 -- so the caller knows its type for sure, which should be of form
  85 --    forall a. C a => <blah>
  86 -- newMethodFromName is supposed to instantiate just the outer
  87 -- type variable and constraint
  88
  89 newMethodFromName origin name inst_ty
  90   = do { id <- tcLookupId name
  91               -- Use tcLookupId not tcLookupGlobalId; the method is almost
  92               -- always a class op, but with -XNoImplicitPrelude GHC is
  93               -- meant to find whatever thing is in scope, and that may
  94               -- be an ordinary function.
  95
  96        ; let (tvs, theta, _caller_knows_this) = tcSplitSigmaTy (idType id)
  97              (the_tv:rest) = tvs
  98              subst = zipOpenTvSubst [the_tv] [inst_ty]
  99
 100        ; wrap <- ASSERT( null rest && isSingleton theta )
 101                  instCall origin [inst_ty] (substTheta subst theta)
 102        ; return (mkHsWrap wrap (HsVar id)) }
 103 \end{code}
 104
 105
 106 %************************************************************************
 107 %*                                                                      *
 108         Deep instantiation and skolemisation
 109 %*                                                                      *
 110 %************************************************************************
 111
 112 Note [Deep skolemisation]
 113 ~~~~~~~~~~~~~~~~~~~~~~~~~
 114 deeplySkolemise decomposes and skolemises a type, returning a type
 115 with all its arrows visible (ie not buried under foralls)
 116
 117 Examples:
 118
 119   deeplySkolemise (Int -> forall a. Ord a => blah)
 120     =  ( wp, [a], [d:Ord a], Int -> blah )
 121     where wp = \x:Int. /\a. \(d:Ord a). <hole> x
 122
 123   deeplySkolemise  (forall a. Ord a => Maybe a -> forall b. Eq b => blah)
 124     =  ( wp, [a,b], [d1:Ord a,d2:Eq b], Maybe a -> blah )
 125     where wp = /\a.\(d1:Ord a).\(x:Maybe a)./\b.\(d2:Ord b). <hole> x
 126
 127 In general,
 128   if      deeplySkolemise ty = (wrap, tvs, evs, rho)
 129     and   e :: rho
 130   then    wrap e :: ty
 131     and   'wrap' binds tvs, evs
 132
 133 ToDo: this eta-abstraction plays fast and loose with termination,
 134       because it can introduce extra lambdas.  Maybe add a `seq` to
 135       fix this
 136
 137
 138 \begin{code}
 139 deeplySkolemise
 140   :: SkolemInfo
 141   -> TcSigmaType
 142   -> TcM (HsWrapper, [TyVar], [EvVar], TcRhoType)
 143
 144 deeplySkolemise skol_info ty
 145   | Just (arg_tys, tvs, theta, ty') <- tcDeepSplitSigmaTy_maybe ty
 146   = do { ids1 <- newSysLocalIds (fsLit "dk") arg_tys
 147        ; tvs1 <- mapM (tcInstSkolTyVar skol_info) tvs
 148        ; let subst = zipTopTvSubst tvs (mkTyVarTys tvs1)
 149        ; ev_vars1 <- newEvVars (substTheta subst theta)
 150        ; (wrap, tvs2, ev_vars2, rho) <- deeplySkolemise skol_info (substTy subst ty')
 151        ; return ( mkWpLams ids1
 152                    <.> mkWpTyLams tvs1
 153                    <.> mkWpLams ev_vars1
 154                    <.> wrap
 155                    <.> mkWpEvVarApps ids1
 156                 , tvs1     ++ tvs2
 157                 , ev_vars1 ++ ev_vars2
 158                 , mkFunTys arg_tys rho ) }
 159
 160   | otherwise
 161   = return (idHsWrapper, [], [], ty)
 162
 163 deeplyInstantiate :: CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
 164 --   Int -> forall a. a -> a  ==>  (\x:Int. [] x alpha) :: Int -> alpha
 165 -- In general if
 166 -- if    deeplyInstantiate ty = (wrap, rho)
 167 -- and   e :: ty
 168 -- then  wrap e :: rho
 169
 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
 177                     <.> wrap2
 178                     <.> wrap1
 179                     <.> mkWpEvVarApps ids1,
 180                  mkFunTys arg_tys rho2) }
 181
 182   | otherwise = return (idHsWrapper, ty)
 183 \end{code}
 184
 185
 186 %************************************************************************
 187 %*                                                                      *
 188             Instantiating a call
 189 %*                                                                      *
 190 %************************************************************************
 191
 192 \begin{code}
 193 ----------------
 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)
 200
 201 instCall orig tys theta
 202   = do  { dict_app <- instCallConstraints orig theta
 203         ; return (dict_app <.> mkWpTyApps tys) }
 204
 205 ----------------
 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.
 209
 210 instCallConstraints _ [] = return idHsWrapper
 211
 212 instCallConstraints origin (EqPred ty1 ty2 : preds)     -- Try short-cut
 213   = do  { traceTc "instCallConstraints" $ ppr (EqPred ty1 ty2)
 214         ; coi   <- unifyType ty1 ty2
 215         ; co_fn <- instCallConstraints origin preds
 216         ; let co = case coi of
 217                        IdCo ty -> ty
 218                        ACo  co -> co
 219         ; return (co_fn <.> WpEvApp (EvCoercion co)) }
 220
 221 instCallConstraints origin (pred : preds)
 222   = do  { ev_var <- emitWanted origin pred
 223         ; co_fn <- instCallConstraints origin preds
 224         ; return (co_fn <.> WpEvApp (EvId ev_var)) }
 225
 226 ----------------
 227 instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
 228 -- Similar to instCall, but only emit the constraints in the LIE
 229 -- Used exclusively for the 'stupid theta' of a data constructor
 230 instStupidTheta orig theta
 231   = do  { _co <- instCallConstraints orig theta -- Discard the coercion
 232         ; return () }
 233 \end{code}
 234
 235 %************************************************************************
 236 %*                                                                      *
 237                 Literals
 238 %*                                                                      *
 239 %************************************************************************
 240
 241 In newOverloadedLit we convert directly to an Int or Integer if we
 242 know that's what we want.  This may save some time, by not
 243 temporarily generating overloaded literals, but it won't catch all
 244 cases (the rest are caught in lookupInst).
 245
 246 \begin{code}
 247 newOverloadedLit :: CtOrigin
 248                  -> HsOverLit Name
 249                  -> TcRhoType
 250                  -> TcM (HsOverLit TcId)
 251 newOverloadedLit orig
 252   lit@(OverLit { ol_val = val, ol_rebindable = rebindable
 253                , ol_witness = meth_name }) res_ty
 254
 255   | not rebindable
 256   , Just expr <- shortCutLit val res_ty
 257         -- Do not generate a LitInst for rebindable syntax.
 258         -- Reason: If we do, tcSimplify will call lookupInst, which
 259         --         will call tcSyntaxName, which does unification,
 260         --         which tcSimplify doesn't like
 261   = return (lit { ol_witness = expr, ol_type = res_ty })
 262
 263   | otherwise
 264   = do  { hs_lit <- mkOverLit val
 265         ; let lit_ty = hsLitType hs_lit
 266         ; fi' <- tcSyntaxOp orig meth_name (mkFunTy lit_ty res_ty)
 267                 -- Overloaded literals must have liftedTypeKind, because
 268                 -- we're instantiating an overloaded function here,
 269                 -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
 270                 -- However this'll be picked up by tcSyntaxOp if necessary
 271         ; let witness = HsApp (noLoc fi') (noLoc (HsLit hs_lit))
 272         ; return (lit { ol_witness = witness, ol_type = res_ty }) }
 273
 274 ------------
 275 mkOverLit :: OverLitVal -> TcM HsLit
 276 mkOverLit (HsIntegral i)
 277   = do  { integer_ty <- tcMetaTy integerTyConName
 278         ; return (HsInteger i integer_ty) }
 279
 280 mkOverLit (HsFractional r)
 281   = do  { rat_ty <- tcMetaTy rationalTyConName
 282         ; return (HsRat r rat_ty) }
 283
 284 mkOverLit (HsIsString s) = return (HsString s)
 285 \end{code}
 286
 287
 288
 289
 290 %************************************************************************
 291 %*                                                                      *
 292                 Re-mappable syntax
 293
 294      Used only for arrow syntax -- find a way to nuke this
 295 %*                                                                      *
 296 %************************************************************************
 297
 298 Suppose we are doing the -XNoImplicitPrelude thing, and we encounter
 299 a do-expression.  We have to find (>>) in the current environment, which is
 300 done by the rename. Then we have to check that it has the same type as
 301 Control.Monad.(>>).  Or, more precisely, a compatible type. One 'customer' had
 302 this:
 303
 304   (>>) :: HB m n mn => m a -> n b -> mn b
 305
 306 So the idea is to generate a local binding for (>>), thus:
 307
 308         let then72 :: forall a b. m a -> m b -> m b
 309             then72 = ...something involving the user's (>>)...
 310         in
 311         ...the do-expression...
 312
 313 Now the do-expression can proceed using then72, which has exactly
 314 the expected type.
 315
 316 In fact tcSyntaxName just generates the RHS for then72, because we only
 317 want an actual binding in the do-expression case. For literals, we can
 318 just use the expression inline.
 319
 320 \begin{code}
 321 tcSyntaxName :: CtOrigin
 322              -> TcType                  -- Type to instantiate it at
 323              -> (Name, HsExpr Name)     -- (Standard name, user name)
 324              -> TcM (Name, HsExpr TcId) -- (Standard name, suitable expression)
 325 --      *** NOW USED ONLY FOR CmdTop (sigh) ***
 326 -- NB: tcSyntaxName calls tcExpr, and hence can do unification.
 327 -- So we do not call it from lookupInst, which is called from tcSimplify
 328
 329 tcSyntaxName orig ty (std_nm, HsVar user_nm)
 330   | std_nm == user_nm
 331   = do rhs <- newMethodFromName orig std_nm ty
 332        return (std_nm, rhs)
 333
 334 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
 335     std_id <- tcLookupId std_nm
 336     let
 337         -- C.f. newMethodAtLoc
 338         ([tv], _, tau)  = tcSplitSigmaTy (idType std_id)
 339         sigma1          = substTyWith [tv] [ty] tau
 340         -- Actually, the "tau-type" might be a sigma-type in the
 341         -- case of locally-polymorphic methods.
 342
 343     addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1) $ do
 344
 345         -- Check that the user-supplied thing has the
 346         -- same type as the standard one.
 347         -- Tiresome jiggling because tcCheckSigma takes a located expression
 348      span <- getSrcSpanM
 349      expr <- tcPolyExpr (L span user_nm_expr) sigma1
 350      return (std_nm, unLoc expr)
 351
 352 syntaxNameCtxt :: HsExpr Name -> CtOrigin -> Type -> TidyEnv
 353                -> TcRn (TidyEnv, SDoc)
 354 syntaxNameCtxt name orig ty tidy_env = do
 355     inst_loc <- getCtLoc orig
 356     let
 357         msg = vcat [ptext (sLit "When checking that") <+> quotes (ppr name) <+>
 358                                 ptext (sLit "(needed by a syntactic construct)"),
 359                     nest 2 (ptext (sLit "has the required type:") <+> ppr (tidyType tidy_env ty)),
 360                     nest 2 (pprArisingAt inst_loc)]
 361     return (tidy_env, msg)
 362 \end{code}
 363
 364
 365 %************************************************************************
 366 %*                                                                      *
 367                 Instances
 368 %*                                                                      *
 369 %************************************************************************
 370
 371 \begin{code}
 372 getOverlapFlag :: TcM OverlapFlag
 373 getOverlapFlag
 374   = do  { dflags <- getDOpts
 375         ; let overlap_ok    = xopt Opt_OverlappingInstances dflags
 376               incoherent_ok = xopt Opt_IncoherentInstances  dflags
 377               overlap_flag | incoherent_ok = Incoherent
 378                            | overlap_ok    = OverlapOk
 379                            | otherwise     = NoOverlap
 380
 381         ; return overlap_flag }
 382
 383 tcGetInstEnvs :: TcM (InstEnv, InstEnv)
 384 -- Gets both the external-package inst-env
 385 -- and the home-pkg inst env (includes module being compiled)
 386 tcGetInstEnvs = do { eps <- getEps; env <- getGblEnv;
 387                      return (eps_inst_env eps, tcg_inst_env env) }
 388
 389 tcExtendLocalInstEnv :: [Instance] -> TcM a -> TcM a
 390   -- Add new locally-defined instances
 391 tcExtendLocalInstEnv dfuns thing_inside
 392  = do { traceDFuns dfuns
 393       ; env <- getGblEnv
 394       ; inst_env' <- foldlM addLocalInst (tcg_inst_env env) dfuns
 395       ; let env' = env { tcg_insts = dfuns ++ tcg_insts env,
 396                          tcg_inst_env = inst_env' }
 397       ; setGblEnv env' thing_inside }
 398
 399 addLocalInst :: InstEnv -> Instance -> TcM InstEnv
 400 -- Check that the proposed new instance is OK,
 401 -- and then add it to the home inst env
 402 addLocalInst home_ie ispec
 403   = do  {       -- Instantiate the dfun type so that we extend the instance
 404                 -- envt with completely fresh template variables
 405                 -- This is important because the template variables must
 406                 -- not overlap with anything in the things being looked up
 407                 -- (since we do unification).
 408                 -- We use tcInstSkolType because we don't want to allocate fresh
 409                 --  *meta* type variables.
 410           let dfun = instanceDFunId ispec
 411         ; (tvs', theta', tau') <- tcInstSkolType InstSkol (idType dfun)
 412         ; let   (cls, tys') = tcSplitDFunHead tau'
 413                 dfun'       = setIdType dfun (mkSigmaTy tvs' theta' tau')
 414                 ispec'      = setInstanceDFunId ispec dfun'
 415
 416                 -- Load imported instances, so that we report
 417                 -- duplicates correctly
 418         ; eps <- getEps
 419         ; let inst_envs = (eps_inst_env eps, home_ie)
 420
 421                 -- Check functional dependencies
 422         ; case checkFunDeps inst_envs ispec' of
 423                 Just specs -> funDepErr ispec' specs
 424                 Nothing    -> return ()
 425
 426                 -- Check for duplicate instance decls
 427         ; let { (matches, _) = lookupInstEnv inst_envs cls tys'
 428               ; dup_ispecs = [ dup_ispec
 429                              | (dup_ispec, _) <- matches
 430                              , let (_,_,_,dup_tys) = instanceHead dup_ispec
 431                              , isJust (tcMatchTys (mkVarSet tvs') tys' dup_tys)] }
 432                 -- Find memebers of the match list which ispec itself matches.
 433                 -- If the match is 2-way, it's a duplicate
 434         ; case dup_ispecs of
 435             dup_ispec : _ -> dupInstErr ispec' dup_ispec
 436             []            -> return ()
 437
 438                 -- OK, now extend the envt
 439         ; return (extendInstEnv home_ie ispec') }
 440
 441 traceDFuns :: [Instance] -> TcRn ()
 442 traceDFuns ispecs
 443   = traceTc "Adding instances:" (vcat (map pp ispecs))
 444   where
 445     pp ispec = ppr (instanceDFunId ispec) <+> colon <+> ppr ispec
 446         -- Print the dfun name itself too
 447
 448 funDepErr :: Instance -> [Instance] -> TcRn ()
 449 funDepErr ispec ispecs
 450   = addDictLoc ispec $
 451     addErr (hang (ptext (sLit "Functional dependencies conflict between instance declarations:"))
 452                2 (pprInstances (ispec:ispecs)))
 453 dupInstErr :: Instance -> Instance -> TcRn ()
 454 dupInstErr ispec dup_ispec
 455   = addDictLoc ispec $
 456     addErr (hang (ptext (sLit "Duplicate instance declarations:"))
 457                2 (pprInstances [ispec, dup_ispec]))
 458
 459 addDictLoc :: Instance -> TcRn a -> TcRn a
 460 addDictLoc ispec thing_inside
 461   = setSrcSpan (mkSrcSpan loc loc) thing_inside
 462   where
 463    loc = getSrcLoc ispec
 464 \end{code}
 465
 466 %************************************************************************
 467 %*                                                                      *
 468         Simple functions over evidence variables
 469 %*                                                                      *
 470 %************************************************************************
 471
 472 \begin{code}
 473 hasEqualities :: [EvVar] -> Bool
 474 -- Has a bunch of canonical constraints (all givens) got any equalities in it?
 475 hasEqualities givens = any (has_eq . evVarPred) givens
 476   where
 477     has_eq (EqPred {})      = True
 478     has_eq (IParam {})      = False
 479     has_eq (ClassP cls tys) = any has_eq (substTheta subst (classSCTheta cls))
 480       where
 481         subst = zipOpenTvSubst (classTyVars cls) tys
 482
 483 ----------------
 484 tyVarsOfWanteds :: WantedConstraints -> TyVarSet
 485 tyVarsOfWanteds = foldrBag (unionVarSet . tyVarsOfWanted) emptyVarSet
 486
 487 tyVarsOfWanted :: WantedConstraint -> TyVarSet
 488 tyVarsOfWanted (WcEvVar wev)   = tyVarsOfWantedEvVar wev
 489 tyVarsOfWanted (WcImplic impl) = tyVarsOfImplication impl
 490
 491 tyVarsOfImplication :: Implication -> TyVarSet
 492 tyVarsOfImplication implic = tyVarsOfWanteds (ic_wanted implic)
 493                              `minusVarSet` (ic_skols implic)
 494
 495 tyVarsOfWantedEvVar :: WantedEvVar -> TyVarSet
 496 tyVarsOfWantedEvVar (WantedEvVar ev _) = tyVarsOfEvVar ev
 497
 498 tyVarsOfWantedEvVars :: Bag WantedEvVar -> TyVarSet
 499 tyVarsOfWantedEvVars = foldrBag (unionVarSet . tyVarsOfWantedEvVar) emptyVarSet
 500
 501 tyVarsOfEvVar :: EvVar -> TyVarSet
 502 tyVarsOfEvVar ev = tyVarsOfPred $ evVarPred ev
 503
 504 tyVarsOfEvVars :: [EvVar] -> TyVarSet
 505 tyVarsOfEvVars = foldr (unionVarSet . tyVarsOfEvVar) emptyVarSet
 506
 507 ---------------
 508 tidyWanteds :: TidyEnv -> WantedConstraints -> WantedConstraints
 509 tidyWanteds env = mapBag (tidyWanted env)
 510
 511 tidyWanted :: TidyEnv -> WantedConstraint -> WantedConstraint
 512 tidyWanted env (WcEvVar wev)     = WcEvVar (tidyWantedEvVar env wev)
 513 tidyWanted env (WcImplic implic) = WcImplic (tidyImplication env implic)
 514
 515 tidyWantedEvVar :: TidyEnv -> WantedEvVar -> WantedEvVar
 516 tidyWantedEvVar env (WantedEvVar ev loc) = WantedEvVar (tidyEvVar env ev) loc
 517
 518 tidyWantedEvVars :: TidyEnv -> Bag WantedEvVar -> Bag WantedEvVar
 519 tidyWantedEvVars env = mapBag (tidyWantedEvVar env)
 520
 521 tidyEvVar :: TidyEnv -> EvVar -> EvVar
 522 tidyEvVar env v = setVarType v (tidyType env (varType v))
 523
 524 tidyImplication :: TidyEnv -> Implication -> Implication
 525 tidyImplication env implic@(Implic { ic_skols = skols, ic_given = given
 526                                    , ic_wanted = wanted })
 527   = implic { ic_skols  = mkVarSet skols'
 528            , ic_given  = map (tidyEvVar env') given
 529            , ic_wanted = tidyWanteds env' wanted }
 530   where
 531     (env', skols') = mapAccumL tidyTyVarBndr env (varSetElems skols)
 532 \end{code}