ghc/compiler/typecheck/GenSpecEtc.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1996
   3 %
   4 \section[GenSpecEtc]{Code for GEN, SPEC, PRED, and REL}
   5
   6 \begin{code}
   7 #include "HsVersions.h"
   8
   9 module GenSpecEtc (
  10         TcSigInfo(..),
  11         genBinds,
  12         checkSigTyVars, checkSigTyVarsGivenGlobals,
  13         specTy
  14     ) where
  15
  16 import Ubiq
  17
  18 import TcMonad
  19 import Inst             ( Inst, InstOrigin(..), LIE(..), plusLIE,
  20                           newDicts, tyVarsOfInst, instToId )
  21 import TcEnv            ( tcGetGlobalTyVars, newMonoIds )
  22 import TcSimplify       ( tcSimplify, tcSimplifyAndCheck, tcSimplifyWithExtraGlobals )
  23 import TcType           ( TcType(..), TcThetaType(..), TcTauType(..),
  24                           TcTyVarSet(..), TcTyVar(..), tcInstType, zonkTcType )
  25
  26 import HsSyn            ( HsBinds(..), Bind(..), MonoBinds(..), HsExpr, OutPat(..),
  27                           Sig, HsLit, ArithSeqInfo, InPat, GRHSsAndBinds, Match, Fake,
  28                           collectBinders )
  29 import TcHsSyn          ( TcIdOcc(..), TcIdBndr(..), TcHsBinds(..), TcBind(..), TcExpr(..) )
  30
  31 import Bag              ( Bag, foldBag, bagToList, listToBag, isEmptyBag )
  32 import Class            ( GenClass )
  33 import Id               ( GenId, Id(..), mkUserId, idType )
  34 import ListSetOps       ( minusList, unionLists, intersectLists )
  35 import Maybes           ( Maybe(..), allMaybes )
  36 import Outputable       ( interppSP, interpp'SP )
  37 import Pretty
  38 import PprType          ( GenClass, GenType, GenTyVar )
  39 import Type             ( mkTyVarTy, splitSigmaTy, mkForAllTys, mkFunTys,
  40                           getTyVar_maybe, tyVarsOfTypes, eqSimpleTheta )
  41 import TyVar            ( GenTyVar, TyVar(..), minusTyVarSet, emptyTyVarSet,
  42                           elementOfTyVarSet, unionTyVarSets, tyVarSetToList )
  43 import Usage            ( UVar(..) )
  44 import Unique           ( Unique )
  45 import Util
  46 \end{code}
  47
  48 %************************************************************************
  49 %*                                                                      *
  50 \subsection[Gen-SignatureInfo]{The @TcSigInfo@ type}
  51 %*                                                                      *
  52 %************************************************************************
  53
  54 A type signature (or user-pragma) is typechecked to produce a
  55 @TcSigInfo@.  It contains @TcTypes@ because they are unified with
  56 the variable's type, and after that checked to see whether they've
  57 been instantiated.
  58
  59 \begin{code}
  60 data TcSigInfo s
  61   = TySigInfo       (TcIdBndr s)        -- for this value...
  62                     [TcTyVar s] (TcThetaType s) (TcTauType s)
  63                     SrcLoc
  64 \end{code}
  65
  66
  67 %************************************************************************
  68 %*                                                                      *
  69 \subsection[Gen-GEN]{Generalising bindings}
  70 %*                                                                      *
  71 %************************************************************************
  72
  73 \begin{code}
  74 genBinds :: [Name]                              -- Binders
  75          -> [TcIdBndr s]                        -- Monomorphic binders
  76          -> TcBind s                            -- Type-checked monobind
  77          -> LIE s                               -- LIE from typecheck of binds
  78          -> [TcSigInfo s]                       -- Signatures, if any
  79          -> (Name -> PragmaInfo)                -- Gives pragma info for binder
  80          -> TcM s (TcHsBinds s, LIE s, [TcIdBndr s])
  81 \end{code}
  82
  83 In the call $(@genBinds@~env~bind~lie~lve)$, $(bind,lie,lve)$
  84 is the result of typechecking a @Bind@.  @genBinds@ implements the BIND-GEN
  85 and BIND-PRED rules.
  86 $lie$ and $lve$ may or may not be
  87 fixed points of the current substitution.
  88
  89 It returns
  90 \begin{itemize}
  91 \item
  92 An @AbsBind@ which wraps up $bind$ in a suitable abstraction.
  93 \item
  94 an LIE, which is the part of the input LIE which isn't discharged by
  95 the AbsBind.  This means the parts which predicate type variables
  96 free in $env$.
  97 \item
  98 An LVE whose domain is identical to that passed in.
  99 Its range is a new set of locals to that passed in,
 100 because they have been gen'd.
 101 \end{itemize}
 102
 103 @genBinds@ takes the
 104 following steps:
 105 \begin{itemize}
 106 \item
 107 find $constrained$, the free variables of $env$.
 108 First we must apply the current substitution to the environment, so that the
 109 correct set of constrained type vars are extracted!
 110 \item
 111 find $free$, the free variables of $lve$ which are not in $constrained$.
 112 We need to apply the current subsitution to $lve$ first, of course.
 113 \item
 114 minimise $lie$ to give $lie'$; all the constraints in $lie'$ are on
 115 single type variables.
 116 \item
 117 split $lie'$ into three: those predicating type variables in $constrained$,
 118 those on type variables in $free$, and the rest.
 119 \item
 120 complain about ``the rest'' part of $lie'$.  These type variables are
 121 ambiguous.
 122 \item
 123 generate new locals for each member of the domain of $lve$, with appropriately
 124 gen'd types.
 125 \item
 126 generate a suitable AbsBinds to enclose the bindings.
 127 \end{itemize}
 128
 129 \begin{code}
 130 genBinds binder_names mono_ids bind lie sig_infos prag_info_fn
 131   =     -- CHECK THAT THE SIGNATURES MATCH
 132         -- Doesn't affect substitution
 133     mapTc checkSigMatch sig_infos       `thenTc_`
 134
 135         -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE IDENTICAL
 136         -- The type signatures on a mutually-recursive group of definitions
 137         -- must all have the same context (or none).
 138         -- We have to zonk them first to make their type variables line up
 139     mapNF_Tc get_zonked_theta sig_infos         `thenNF_Tc` \ thetas ->
 140     checkTc (null thetas || all (eqSimpleTheta (head thetas)) (tail thetas))
 141             (sigContextsErr sig_infos)          `thenTc_`
 142
 143         -- COMPUTE VARIABLES OVER WHICH TO QUANTIFY, namely tyvars_to_gen
 144     mapNF_Tc (zonkTcType . idType) mono_ids     `thenNF_Tc` \ mono_id_types ->
 145     tcGetGlobalTyVars                           `thenNF_Tc` \ free_tyvars ->
 146     let
 147         mentioned_tyvars = tyVarsOfTypes mono_id_types
 148         tyvars_to_gen    = mentioned_tyvars `minusTyVarSet` free_tyvars
 149     in
 150
 151         -- DEAL WITH OVERLOADING
 152     resolveOverloading tyvars_to_gen lie bind sig_infos
 153                  `thenTc` \ (lie', reduced_tyvars_to_gen, dict_binds, dicts_bound) ->
 154
 155          -- BUILD THE NEW LOCALS
 156     let
 157         tyvars      = tyVarSetToList reduced_tyvars_to_gen      -- Commit to a particular order
 158         dict_tys    = [idType d | TcId d <- dicts_bound]        -- Slightly ugh-ish
 159         poly_tys    = map (mkForAllTys tyvars . mkFunTys dict_tys) mono_id_types
 160         poly_ids    = zipWithEqual mk_poly binder_names poly_tys
 161         mk_poly name ty = mkUserId name ty (prag_info_fn name)
 162     in
 163          -- BUILD RESULTS
 164     returnTc (
 165          AbsBinds tyvars
 166                   dicts_bound
 167                   (map TcId mono_ids `zip` map TcId poly_ids)
 168                   dict_binds
 169                   bind,
 170          lie',
 171          poly_ids
 172     )
 173
 174 get_zonked_theta (TySigInfo _ _ theta _ _)
 175   = mapNF_Tc (\ (c,t) -> zonkTcType t `thenNF_Tc` \ t' -> returnNF_Tc (c,t')) theta
 176 \end{code}
 177
 178
 179 \begin{code}
 180 resolveOverloading
 181         :: TcTyVarSet s         -- Tyvars over which we are going to generalise
 182         -> LIE s                -- The LIE to deal with
 183         -> TcBind s             -- The binding group
 184         -> [TcSigInfo s]        -- And its real type-signature information
 185         -> TcM s (LIE s,                        -- LIE to pass up the way; a fixed point of
 186                                                 -- the current substitution
 187                   TcTyVarSet s,                 -- Revised tyvars to generalise
 188                   [(TcIdOcc s, TcExpr s)],      -- Dict bindings
 189                   [TcIdOcc s])                  -- List of dicts to bind here
 190
 191 resolveOverloading tyvars_to_gen dicts bind ty_sigs
 192   | not (isUnRestrictedGroup tysig_vars bind)
 193   =     -- Restricted group, so bind no dictionaries, and
 194         -- remove from tyvars_to_gen any constrained type variables
 195
 196         -- *Don't* simplify dicts at this point, because we aren't going
 197         -- to generalise over these dicts.  By the time we do simplify them
 198         -- we may well know more.  For example (this actually came up)
 199         --      f :: Array Int Int
 200         --      f x = array ... xs where xs = [1,2,3,4,5]
 201         -- We don't want to generate lots of (fromInt Int 1), (fromInt Int 2)
 202         -- stuff.  If we simplify only at the f-binding (not the xs-binding)
 203         -- we'll know that the literals are all Ints, and we can just produce
 204         -- Int literals!
 205
 206         -- Find all the type variables involved in overloading, the "constrained_tyvars"
 207         -- These are the ones we *aren't* going to generalise.
 208         -- We must be careful about doing this:
 209         --  (a) If we fail to generalise a tyvar which is not actually
 210         --      constrained, then it will never, ever get bound, and lands
 211         --      up printed out in interface files!  Notorious example:
 212         --              instance Eq a => Eq (Foo a b) where ..
 213         --      Here, b is not constrained, even though it looks as if it is.
 214         --      Another, more common, example is when there's a Method inst in
 215         --      the LIE, whose type might very well involve non-overloaded
 216         --      type variables.
 217         --  (b) On the other hand, we mustn't generalise tyvars which are constrained,
 218         --      because we are going to pass on out the unmodified LIE, with those
 219         --      tyvars in it.  They won't be in scope if we've generalised them.
 220         --
 221         -- So we are careful, and do a complete simplification just to find the
 222         -- constrained tyvars. We don't use any of the results, except to
 223         -- find which tyvars are constrained.
 224
 225         tcSimplify tyvars_to_gen dicts      `thenTc` \ (_, _, dicts_sig) ->
 226         let
 227           -- ASSERT: dicts_sig is already zonked!
 228           constrained_tyvars    = foldBag unionTyVarSets tyVarsOfInst emptyTyVarSet dicts_sig
 229           reduced_tyvars_to_gen = tyvars_to_gen `minusTyVarSet` constrained_tyvars
 230         in
 231
 232         -- Do it again, but with increased free_tyvars/reduced_tyvars_to_gen:
 233         -- We still need to do this simplification, because some dictionaries
 234         -- may gratuitouslyconstrain some tyvars over which we *are* going
 235         -- to generalise.
 236         -- For example d::Eq (Foo a b), where Foo is instanced as above.
 237         tcSimplifyWithExtraGlobals constrained_tyvars reduced_tyvars_to_gen dicts
 238                                     `thenTc` \ (dicts_free, dicts_binds, dicts_sig2) ->
 239         ASSERT(isEmptyBag dicts_sig2)
 240
 241         returnTc (dicts_free,                   -- All these are left unbound
 242                   reduced_tyvars_to_gen,
 243                   dicts_binds,                  -- Local dict binds
 244                   [])                           -- No lambda-bound dicts
 245
 246                 -- The returned LIE should be a fixed point of the substitution
 247
 248   | otherwise   -- An unrestricted group
 249   = case ty_sigs of
 250         [] ->   -- NO TYPE SIGNATURES
 251
 252             tcSimplify tyvars_to_gen dicts  `thenTc` \ (dicts_free, dict_binds, dicts_sig) ->
 253             returnTc (dicts_free, tyvars_to_gen, dict_binds,
 254                       map instToId (bagToList dicts_sig))
 255
 256         (TySigInfo _ _ theta _ _ : other) -> -- TYPE SIGNATURES PRESENT!
 257
 258             tcAddErrCtxt (sigsCtxt tysig_vars) $
 259
 260             newDicts SignatureOrigin theta      `thenNF_Tc` \ (dicts_sig, dict_ids) ->
 261
 262                     -- Check that the needed dicts can be expressed in
 263                     -- terms of the signature ones
 264             tcSimplifyAndCheck
 265                 tyvars_to_gen   -- Type vars over which we will quantify
 266                 dicts_sig       -- Available dicts
 267                 dicts           -- Want bindings for these dicts
 268
 269                                     `thenTc` \ (dicts_free, dict_binds) ->
 270
 271             returnTc (dicts_free, tyvars_to_gen, dict_binds, dict_ids)
 272   where
 273     tysig_vars   = [sig_var | (TySigInfo sig_var _ _ _ _) <- ty_sigs]
 274 \end{code}
 275
 276 @checkSigMatch@ does the next step in checking signature matching.
 277 The tau-type part has already been unified.  What we do here is to
 278 check that this unification has not over-constrained the (polymorphic)
 279 type variables of the original signature type.
 280
 281 The error message here is somewhat unsatisfactory, but it'll do for
 282 now (ToDo).
 283
 284 \begin{code}
 285 checkSigMatch :: TcSigInfo s -> TcM s [TcTyVar s]
 286
 287 checkSigMatch (TySigInfo id sig_tyvars _ tau_ty src_loc)
 288   = tcAddSrcLoc src_loc $
 289     tcAddErrCtxt (sigCtxt id) $
 290     checkSigTyVars sig_tyvars tau_ty (idType id)
 291 \end{code}
 292
 293
 294 %************************************************************************
 295 %*                                                                      *
 296 \subsection[GenEtc-monomorphism]{The monomorphism restriction}
 297 %*                                                                      *
 298 %************************************************************************
 299
 300 Not exported:
 301
 302 \begin{code}
 303 isUnRestrictedGroup :: [TcIdBndr s]             -- Signatures given for these
 304                     -> TcBind s
 305                     -> Bool
 306
 307 isUnRestrictedGroup sigs EmptyBind              = True
 308 isUnRestrictedGroup sigs (NonRecBind monobinds) = isUnResMono sigs monobinds
 309 isUnRestrictedGroup sigs (RecBind monobinds)    = isUnResMono sigs monobinds
 310
 311 is_elem v vs = isIn "isUnResMono" v vs
 312
 313 isUnResMono sigs (PatMonoBind (VarPat (TcId v)) _ _)    = v `is_elem` sigs
 314 isUnResMono sigs (PatMonoBind other      _ _)           = False
 315 isUnResMono sigs (VarMonoBind (TcId v) _)               = v `is_elem` sigs
 316 isUnResMono sigs (FunMonoBind _ _ _)                    = True
 317 isUnResMono sigs (AndMonoBinds mb1 mb2)                 = isUnResMono sigs mb1 &&
 318                                                           isUnResMono sigs mb2
 319 isUnResMono sigs EmptyMonoBinds                         = True
 320 \end{code}
 321
 322
 323 %************************************************************************
 324 %*                                                                      *
 325 \subsection[GenEtc-sig]{Matching a type signature}
 326 %*                                                                      *
 327 %************************************************************************
 328
 329 @checkSigTyVars@ is used after the type in a type signature has been unified with
 330 the actual type found.  It then checks that the type variables of the type signature
 331 are
 332         (a) still all type variables
 333                 eg matching signature [a] against inferred type [(p,q)]
 334                 [then a will be unified to a non-type variable]
 335
 336         (b) still all distinct
 337                 eg matching signature [(a,b)] against inferred type [(p,p)]
 338                 [then a and b will be unified together]
 339
 340         (c) not mentioned in the environment
 341                 eg the signature for f in this:
 342
 343                         g x = ... where
 344                                         f :: a->[a]
 345                                         f y = [x,y]
 346
 347                 Here, f is forced to be monorphic by the free occurence of x.
 348
 349 Before doing this, the substitution is applied to the signature type variable.
 350
 351 \begin{code}
 352 checkSigTyVars :: [TcTyVar s]           -- The original signature type variables
 353                -> TcType s              -- signature type (for err msg)
 354                -> TcType s              -- inferred type (for err msg)
 355                -> TcM s [TcTyVar s]     -- Post-substitution signature type variables
 356
 357 checkSigTyVars sig_tyvars sig_tau inferred_tau
 358   = tcGetGlobalTyVars                   `thenNF_Tc` \ env_tyvars ->
 359     checkSigTyVarsGivenGlobals env_tyvars sig_tyvars sig_tau inferred_tau
 360
 361 checkSigTyVarsGivenGlobals
 362          :: TcTyVarSet s        -- Consider these fully-zonked tyvars as global
 363          -> [TcTyVar s]         -- The original signature type variables
 364          -> TcType s            -- signature type (for err msg)
 365          -> TcType s            -- inferred type (for err msg)
 366          -> TcM s [TcTyVar s]   -- Post-substitution signature type variables
 367
 368 checkSigTyVarsGivenGlobals globals sig_tyvars sig_tau inferred_tau
 369   =      -- Check point (a) above
 370     mapNF_Tc (zonkTcType.mkTyVarTy) sig_tyvars                          `thenNF_Tc` \ sig_tys ->
 371     checkMaybeTcM (allMaybes (map getTyVar_maybe sig_tys)) match_err    `thenTc` \ sig_tyvars' ->
 372
 373          -- Check point (b)
 374     checkTcM (hasNoDups sig_tyvars') match_err          `thenTc_`
 375
 376         -- Check point (c)
 377         -- We want to report errors in terms of the original signature tyvars,
 378         -- ie sig_tyvars, NOT sig_tyvars'.  sig_tys and sig_tyvars' correspond
 379         -- 1-1 with sig_tyvars, so we can just map back.
 380     let
 381         mono_tyvars = [ sig_tyvar
 382                       | (sig_tyvar,sig_tyvar') <- zipEqual sig_tyvars sig_tyvars',
 383                         sig_tyvar' `elementOfTyVarSet` globals
 384                       ]
 385     in
 386     checkTc (null mono_tyvars)
 387             (notAsPolyAsSigErr sig_tau mono_tyvars)     `thenTc_`
 388
 389     returnTc sig_tyvars'
 390   where
 391     match_err = zonkTcType inferred_tau `thenNF_Tc` \ inferred_tau' ->
 392                 failTc (badMatchErr sig_tau inferred_tau')
 393 \end{code}
 394
 395
 396 %************************************************************************
 397 %*                                                                      *
 398 \subsection[GenEtc-SpecTy]{Instantiate a type and create new dicts for it}
 399 %*                                                                      *
 400 %************************************************************************
 401
 402 \begin{code}
 403 specTy :: InstOrigin s
 404        -> Type
 405        -> NF_TcM s ([TcTyVar s], LIE s, TcType s, [TcIdOcc s])
 406
 407 specTy origin sigma_ty
 408   = tcInstType [] sigma_ty              `thenNF_Tc` \ tc_sigma_ty ->
 409     let
 410         (tyvars, theta, tau) = splitSigmaTy tc_sigma_ty
 411     in
 412          -- Instantiate the dictionary types
 413     newDicts origin theta               `thenNF_Tc` \ (dicts, dict_ids) ->
 414
 415          -- Return the list of tyvars, the list of dicts and the tau type
 416     returnNF_Tc (tyvars, dicts, tau, dict_ids)
 417 \end{code}
 418
 419
 420
 421 Contexts and errors
 422 ~~~~~~~~~~~~~~~~~~~
 423 \begin{code}
 424 notAsPolyAsSigErr sig_tau mono_tyvars sty
 425   = ppHang (ppStr "A type signature is more polymorphic than the inferred type")
 426         4  (ppAboves [ppStr "(That is, one or more type variables in the inferred type can't be forall'd.)",
 427                       ppHang (ppStr "Monomorphic type variable(s):")
 428                            4 (interpp'SP sty mono_tyvars),
 429                       ppStr "Possible cause: the RHS mentions something subject to the monomorphism restriction"
 430                      ])
 431 \end{code}
 432
 433
 434 \begin{code}
 435 badMatchErr sig_ty inferred_ty sty
 436   = ppHang (ppStr "Type signature doesn't match inferred type")
 437          4 (ppAboves [ppHang (ppStr "Signature:") 4 (ppr sty sig_ty),
 438                       ppHang (ppStr "Inferred :") 4 (ppr sty inferred_ty)
 439            ])
 440
 441 sigCtxt id sty
 442   = ppSep [ppStr "When checking signature for", ppr sty id]
 443 sigsCtxt ids sty
 444   = ppSep [ppStr "When checking signature(s) for:", interpp'SP sty ids]
 445 \end{code}
 446
 447
 448 \begin{code}
 449 sigContextsErr ty_sigs sty
 450   = ppHang (ppStr "A group of type signatures have mismatched contexts")
 451          4 (ppAboves (map ppr_sig_info ty_sigs))
 452   where
 453     ppr_sig_info (TySigInfo val tyvars theta tau_ty _)
 454       = ppHang (ppBeside (ppr sty val) (ppStr " :: "))
 455              4 (if null theta
 456                 then ppNil
 457                 else ppBesides [ppStr "(",
 458                                 ppIntersperse (ppStr ", ") (map (ppr_inst sty) theta),
 459                                 ppStr ") => ..."])
 460     ppr_inst sty (clas, ty) = ppCat [ppr sty clas, ppr sty ty]
 461 \end{code}