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