ghc/compiler/typecheck/GenSpecEtc.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1995
   3 %
   4 \section[GenSpecEtc]{Code for GEN, SPEC, PRED, and REL}
   5
   6 \begin{code}
   7 #include "HsVersions.h"
   8
   9 module GenSpecEtc (
  10         genBinds, SignatureInfo(..),
  11         checkSigTyVars,
  12
  13         -- and to make the interface self-sufficient...
  14         Bag, E, Bind, Binds, TypecheckedPat, Id, Inst,
  15         LIE, TcResult, Name, SrcLoc, Subst, TyVar, UniType,
  16         UniqueSupply, Error(..), Pretty(..), PprStyle,
  17         PrettyRep
  18     ) where
  19
  20 import TcMonad          -- typechecker monadery
  21 import TcMonadFns       ( applyTcSubstAndCollectTyVars,
  22                           mkIdsWithGivenTys
  23                         )
  24 import AbsSyn
  25
  26 import AbsUniType
  27 import E                ( tvOfE, E, LVE(..), TCE(..), UniqFM, CE(..) )
  28                         -- TCE and CE for pragmas only
  29 import Errors
  30 import Id               ( getIdUniType, mkInstId, Id, DictVar(..) )
  31 import IdInfo
  32 import Inst
  33 import LIE              ( mkLIE, unMkLIE, LIE )
  34 import ListSetOps       ( minusList, unionLists, intersectLists )
  35 import Maybes           ( assocMaybe, Maybe(..) )
  36 import Name             ( Name(..) )    -- ToDo: a HACK
  37 import TcSimplify       ( tcSimplify, tcSimplifyAndCheck )
  38 import Util
  39
  40 IMPORT_Trace            -- ToDo: rm (debugging)
  41 import Pretty           --
  42 \end{code}
  43
  44 %************************************************************************
  45 %*                                                                      *
  46 \subsection[Gen-SignatureInfo]{The @SignatureInfo@ type}
  47 %*                                                                      *
  48 %************************************************************************
  49
  50 A type signature (or user-pragma) is typechecked to produce a
  51 @SignatureInfo@.
  52
  53 \begin{code}
  54 data SignatureInfo
  55   = TySigInfo       Id  -- for this value...
  56                     [TyVar] [Inst] TauType
  57                     SrcLoc
  58
  59   | ValSpecInfo     Name        -- we'd rather have the Name than Id...
  60                     UniType
  61                     (Maybe Name)
  62                     SrcLoc
  63
  64   | ValInlineInfo   Name
  65                     UnfoldingGuidance
  66                     SrcLoc
  67
  68   | ValDeforestInfo Name
  69                     SrcLoc
  70
  71   | ValMagicUnfoldingInfo
  72                     Name
  73                     FAST_STRING
  74                     SrcLoc
  75
  76   -- ToDo: perhaps add more (for other user pragmas)
  77 \end{code}
  78
  79
  80 %************************************************************************
  81 %*                                                                      *
  82 \subsection[Gen-GEN]{Generalising bindings}
  83 %*                                                                      *
  84 %************************************************************************
  85
  86 \begin{code}
  87 genBinds :: Bool                                -- True <=> top level
  88          -> E
  89          -> TypecheckedBind
  90          -> LIE                                 -- LIE from typecheck of binds
  91          -> LVE                                 -- Local types
  92          -> [SignatureInfo]                     -- Signatures, if any
  93          -> TcM (TypecheckedBinds, LIE, LVE)    -- Generalised binds, reduced LIE,
  94                                                 --      polymorphic LVE
  95                                                 -- The LVE and LIE are fixed points
  96                                                 -- of the substitution
  97 \end{code}
  98
  99 In the call $(@genBinds@~env~bind~lie~lve)$, $(bind,lie,lve)$
 100 is the result of typechecking a @Bind@.  @genBinds@ implements the BIND-GEN
 101 and BIND-PRED rules.
 102 $lie$ and $lve$ may or may not be
 103 fixed points of the current substitution.
 104
 105 It returns
 106 \begin{itemize}
 107 \item
 108 An @AbsBind@ which wraps up $bind$ in a suitable abstraction.
 109 \item
 110 an LIE, which is the part of the input LIE which isn't discharged by
 111 the AbsBind.  This means the parts which predicate type variables
 112 free in $env$.
 113 \item
 114 An LVE whose domain is identical to that passed in.
 115 Its range is a new set of locals to that passed in,
 116 because they have been gen'd.
 117 \end{itemize}
 118
 119 @genBinds@ takes the
 120 following steps:
 121 \begin{itemize}
 122 \item
 123 find $constrained$, the free variables of $env$.
 124 First we must apply the current substitution to the environment, so that the
 125 correct set of constrained type vars are extracted!
 126 \item
 127 find $free$, the free variables of $lve$ which are not in $constrained$.
 128 We need to apply the current subsitution to $lve$ first, of course.
 129 \item
 130 minimise $lie$ to give $lie'$; all the constraints in $lie'$ are on
 131 single type variables.
 132 \item
 133 split $lie'$ into three: those predicating type variables in $constrained$,
 134 those on type variables in $free$, and the rest.
 135 \item
 136 complain about ``the rest'' part of $lie'$.  These type variables are
 137 ambiguous.
 138 \item
 139 generate new locals for each member of the domain of $lve$, with appropriately
 140 gen'd types.
 141 \item
 142 generate a suitable AbsBinds to enclose the bindings.
 143 \end{itemize}
 144
 145 \begin{code}
 146 genBinds top_level e bind lie lve sigs
 147   = getSrcLocTc                                 `thenNF_Tc` \ locn ->
 148
 149         -- GET TYPE VARIABLES FREE IN ENV
 150     applyTcSubstAndCollectTyVars (tvOfE e)      `thenNF_Tc` \ free_tyvars ->
 151
 152         -- CHECK THAT THE SIGNATURES MATCH
 153         -- Doesn't affect substitution
 154     mapTc (checkSigMatch free_tyvars) sigs      `thenTc_`
 155
 156          -- UNPACK THE LVE
 157     let
 158         (bound_var_names, bound_var_locals) = unzip lve
 159         bound_var_types = map getIdUniType bound_var_locals
 160     in
 161     applyTcSubstToTys bound_var_types `thenNF_Tc`       \ bound_var_types' ->
 162     let
 163         mentioned_tyvars' = extractTyVarsFromTys bound_var_types'
 164
 165          -- COMPUTE VARIABLES OVER WHICH TO QUANTIFY, namely tyvars_to_gen
 166         tyvars_to_gen = mentioned_tyvars' `minusList` free_tyvars
 167
 168         -- UNSCRAMBLE "sigs" INTO VARIOUS FLAVOURS
 169         -- AND SNAFFLE ANY "IdInfos" FOR VARS HERE
 170
 171         (ty_sigs, upragmas) = partition is_tysig_info sigs
 172         inline_sigs         = filter is_inline_info   upragmas
 173         deforest_sigs       = filter is_deforest_info upragmas
 174         magic_uf_sigs       = filter is_magic_uf_info upragmas
 175         spec_sigs           = filter is_spec_info     upragmas
 176
 177         unfold_me_fn n
 178           = case [ x | x@(ValInlineInfo v _ _) <- inline_sigs, v == n ] of
 179               (ValInlineInfo _ guide _ :_) -> iWantToBeINLINEd guide
 180               [] ->
 181                 case [ x | x@(ValMagicUnfoldingInfo v _ _) <- magic_uf_sigs, v == n ] of
 182                   (ValMagicUnfoldingInfo _ str _:_) -> mkMagicUnfolding str
 183                   []                            -> noInfo_UF
 184
 185         deforest_me_fn n
 186           = case [ x | x@(ValDeforestInfo v _) <- deforest_sigs, v == n ] of
 187             (ValDeforestInfo _ _ : _) -> DoDeforest
 188             [] -> Don'tDeforest
 189
 190         id_info_for n
 191           = noIdInfo
 192               `addInfo_UF` (unfold_me_fn   n)
 193               `addInfo`    (deforest_me_fn n)
 194
 195         id_infos = [ id_info_for n | n <- bound_var_names ]
 196     in
 197     resolveOverloading top_level e free_tyvars tyvars_to_gen lie bind ty_sigs
 198                  `thenTc` \ (lie', reduced_tyvars_to_gen, dict_binds, dicts_bound) ->
 199
 200          -- BUILD THE NEW LOCALS
 201     let
 202         dict_tys = map getInstUniType dicts_bound
 203
 204         envs_and_new_locals_types
 205           = map (quantifyTy reduced_tyvars_to_gen . glueTyArgs dict_tys) bound_var_types'
 206
 207         (_, new_locals_types) = unzip envs_and_new_locals_types
 208     in
 209          -- The new_locals function is passed into genBinds
 210          -- so it can generate top-level or non-top-level locals
 211     let
 212         lve_of_new_ids = mkIdsWithGivenTys bound_var_names new_locals_types id_infos
 213         new_ids = map snd lve_of_new_ids
 214     in
 215          -- BUILD RESULTS
 216     returnTc (
 217 --      pprTrace "Gen: " (ppSep [ppr PprDebug new_ids,
 218 --                               ppStr "; to gen ", ppr PprDebug tyvars_to_gen,
 219 --                               ppStr "; reduced ", ppr PprDebug reduced_tyvars_to_gen
 220 --              ]) $
 221          AbsBinds reduced_tyvars_to_gen (map mkInstId dicts_bound)
 222                  (bound_var_locals `zip` new_ids)
 223                  dict_binds bind,
 224          lie',
 225          lve_of_new_ids
 226     )
 227   where
 228     is_tysig_info (TySigInfo _ _ _ _ _) = True
 229     is_tysig_info _                     = False
 230
 231     is_inline_info (ValInlineInfo _ _ _) = True
 232     is_inline_info _ = False
 233
 234     is_deforest_info (ValDeforestInfo _ _) = True
 235     is_deforest_info _ = False
 236
 237     is_magic_uf_info (ValMagicUnfoldingInfo _ _ _) = True
 238     is_magic_uf_info _ = False
 239
 240     is_spec_info (ValSpecInfo _ _ _ _) = True
 241     is_spec_info _ = False
 242 \end{code}
 243
 244
 245 \begin{code}
 246 resolveOverloading
 247         :: Bool                 -- True <=> top level
 248         -> E
 249         -> [TyVar]              -- Tyvars free in E
 250         -> [TyVar]              -- Tyvars over which we are going to generalise
 251         -> LIE                  -- The LIE to deal with
 252         -> TypecheckedBind      -- The binding group
 253         -> [SignatureInfo]      -- And its real type-signature information
 254         -> TcM (LIE,                    -- LIE to pass up the way; a fixed point of
 255                                         -- the current substitution
 256                 [TyVar],                -- Revised tyvars to generalise
 257                 [(Inst, TypecheckedExpr)],-- Dict bindings
 258                 [Inst])                 -- List of dicts to bind here
 259
 260 resolveOverloading top_level e free_tyvars tyvars_to_gen lie bind ty_sigs
 261   = let
 262         dicts = unMkLIE lie
 263     in
 264          -- DEAL WITH MONOMORPHISM RESTRICTION
 265     if (not (isUnRestrictedGroup tysig_vars bind)) then
 266
 267         -- Restricted group, so bind no dictionaries, and
 268         -- remove from tyvars_to_gen any constrained type variables
 269
 270         -- *Don't* simplify dicts at this point, because we aren't going
 271         -- to generalise over these dicts.  By the time we do simplify them
 272         -- we may well know more.  For example (this actually came up)
 273         --      f :: Array Int Int
 274         --      f x = array ... xs where xs = [1,2,3,4,5]
 275         -- We don't want to generate lots of (fromInt Int 1), (fromInt Int 2)
 276         -- stuff.  If we simplify only at the f-binding (not the xs-binding)
 277         -- we'll know that the literals are all Ints, and we can just produce
 278         -- Int literals!
 279
 280         -- Find all the type variables involved in overloading
 281         -- These are the ones we *aren't* going to generalise.
 282         -- We must be careful about doing this:
 283         --  (a) If we fail to generalise a tyvar which is not actually
 284         --      constrained, then it will never, ever get bound, and lands
 285         --      up printed out in interface files!  Notorious example:
 286         --              instance Eq a => Eq (Foo a b) where ..
 287         --      Here, b is not constrained, even though it looks as if it is.
 288         --      Another, more common, example is when there's a Method inst in
 289         --      the LIE, whose type might very well involve non-overloaded
 290         --      type variables.
 291         --  (b) On the other hand, we mustn't generalise tyvars which are constrained,
 292         --      because we are going to pass on out the unmodified LIE, with those
 293         --      tyvars in it.  They won't be in scope if we've generalised them.
 294         --
 295         -- So we are careful, and do a complete simplification just to find the
 296         -- constrained tyvars. We don't use any of the results, except to
 297         -- find which tyvars are constrained.
 298
 299         tcSimplify top_level free_tyvars tyvars_to_gen dicts
 300                                     `thenTc` \ (_, _, dicts_sig) ->
 301
 302 -- ASSERT: tcSimplify has already applied subst to its results
 303 -- (WDP/SLPJ 95/07)
 304 --      applyTcSubstToInsts dicts_sig   `thenNF_Tc`     \ dicts_sig' ->
 305         let
 306           constrained_tyvars
 307             = foldr (unionLists . extractTyVarsFromInst) [] dicts_sig
 308
 309           reduced_tyvars_to_gen = tyvars_to_gen `minusList` constrained_tyvars
 310
 311           increased_free_tyvars = free_tyvars `unionLists` constrained_tyvars
 312         in
 313
 314         -- Do it again, but with increased_free_tyvars/reduced_tyvars_to_gen:
 315
 316         tcSimplify top_level increased_free_tyvars reduced_tyvars_to_gen dicts
 317                                     `thenTc` \ (dicts_free, dicts_binds, dicts_sig2) ->
 318 --NB: still no applyTcSubstToInsts
 319
 320 --      pprTrace "resolve:" (ppCat [ppr PprDebug free_tyvars, ppr PprDebug tyvars_to_gen, ppr PprDebug constrained_tyvars, ppr PprDebug reduced_tyvars_to_gen, ppr PprDebug bind]) $
 321         returnTc (mkLIE (dicts_free++dicts_sig2), -- All these are left unbound
 322                   reduced_tyvars_to_gen,
 323                   dicts_binds,                  -- Local dict binds
 324                   [])                           -- No lambda-bound dicts
 325
 326                 -- The returned LIE should be a fixed point of the substitution
 327
 328     else -- Unrestricted group
 329        case ty_sigs of
 330          [] ->  -- NO TYPE SIGNATURES
 331
 332             tcSimplify top_level free_tyvars tyvars_to_gen dicts
 333                                     `thenTc` \ (dicts_free, dict_binds, dicts_sig) ->
 334             returnTc (mkLIE dicts_free, tyvars_to_gen, dict_binds, dicts_sig)
 335
 336          other -> -- TYPE SIGNATURES PRESENT!
 337
 338                 -- Check that all the signature contexts are identical
 339                 -- "tysig_dicts_s" is a list (one for each id declared
 340                 -- in this group) of lists of dicts (the list
 341                 -- corresponds to the context in the sig).
 342                 -- "dicts_sig" is just the first such list; we match
 343                 -- it against all the others.
 344
 345             mapNF_Tc applyTcSubstToInsts tysig_dicts_s
 346                                 `thenNF_Tc` \ (dicts_sig : other_dicts_s) ->
 347
 348             checkTc (not (all (same_dicts dicts_sig) other_dicts_s))
 349                 -- The type signatures on a mutually-recursive group of definitions
 350                 -- must all have the same context (or none).  See Errors.lhs.
 351                 (sigContextsErr ty_sigs) `thenTc_`
 352
 353                     -- Check that the needed dicts can be expressed in
 354                     -- terms of the signature ones
 355             tcSimplifyAndCheck
 356                 top_level
 357                 free_tyvars     -- Vars free in the environment
 358                 tyvars_to_gen   -- Type vars over which we will quantify
 359                 dicts_sig       -- Available dicts
 360                 dicts           -- Want bindings for these dicts
 361                 (BindSigCtxt tysig_vars)
 362
 363                                     `thenTc` \ (dicts_free, dict_binds) ->
 364
 365             returnTc (mkLIE dicts_free, tyvars_to_gen, dict_binds, dicts_sig)
 366   where
 367     tysig_dicts_s = [dicts   | (TySigInfo _       _ dicts _ _) <- ty_sigs]
 368     tysig_vars    = [sig_var | (TySigInfo sig_var _ _     _ _) <- ty_sigs]
 369
 370         -- same_dicts checks that (post substitution) all the type signatures
 371         -- constrain the same type variables in the same way
 372     same_dicts []       []       = True
 373     same_dicts []       _        = False
 374     same_dicts _        []       = False
 375     same_dicts (d1:d1s) (d2:d2s) = matchesInst d1 d2 && same_dicts d1s d2s
 376
 377     -- don't use the old version, because zipWith will truncate
 378     -- the longer one!
 379     --OLD: same_dicts dicts1 dicts2 = and (zipWith matchesInst dicts1 dicts2)
 380 \end{code}
 381
 382 @checkSigMatch@ does the next step in checking signature matching.
 383 The tau-type part has already been unified.  What we do here is to
 384 check that this unification has not over-constrained the (polymorphic)
 385 type variables of the original signature type.
 386
 387 The error message here is somewhat unsatisfactory, but it'll do for
 388 now (ToDo).
 389
 390 \begin{code}
 391 checkSigMatch :: [TyVar]        -- Free in environment
 392               -> SignatureInfo
 393               -> TcM [TyVar]
 394
 395 checkSigMatch env_tyvars (TySigInfo name sig_tyvars _ tau_ty src_loc)
 396   = let
 397         inferred_ty = getIdUniType name
 398     in
 399     addSrcLocTc src_loc (
 400     checkSigTyVars env_tyvars sig_tyvars tau_ty inferred_ty
 401                    (SigCtxt name tau_ty)
 402     )
 403
 404 checkSigMatch _ other_not_really_a_sig = returnTc []
 405 \end{code}
 406
 407
 408 %************************************************************************
 409 %*                                                                      *
 410 \subsection[GenEtc-monomorphism]{The monomorphism restriction}
 411 %*                                                                      *
 412 %************************************************************************
 413
 414 Not exported:
 415
 416 \begin{code}
 417 isUnRestrictedGroup :: [Id]             -- Signatures given for these
 418                      -> TypecheckedBind
 419                      -> Bool
 420
 421 isUnRestrictedGroup sigs EmptyBind              = True
 422 isUnRestrictedGroup sigs (NonRecBind monobinds) = isUnResMono sigs monobinds
 423 isUnRestrictedGroup sigs (RecBind monobinds)    = isUnResMono sigs monobinds
 424
 425 is_elem = isIn "isUnResMono"
 426
 427 isUnResMono sigs EmptyMonoBinds = True
 428 isUnResMono sigs (AndMonoBinds mb1 mb2) = isUnResMono sigs mb1 && isUnResMono sigs mb2
 429 isUnResMono sigs (PatMonoBind (VarPat v) _ _)   = v `is_elem` sigs
 430 isUnResMono sigs (PatMonoBind other      _ _)   = False
 431 isUnResMono sigs (VarMonoBind v _)              = v `is_elem` sigs
 432 isUnResMono sigs (FunMonoBind _ _ _)            = True
 433 \end{code}
 434
 435
 436 %************************************************************************
 437 %*                                                                      *
 438 \subsection[GenEtc-sig]{Matching a type signature}
 439 %*                                                                      *
 440 %************************************************************************
 441
 442 @checkSigTyVars@ is used after the type in a type signature has been unified with
 443 the actual type found.  It then checks that the type variables of the type signature
 444 are
 445         (a) still all type variables
 446                 eg matching signature [a] against inferred type [(p,q)]
 447                 [then a will be unified to a non-type variable]
 448
 449         (b) still all distinct
 450                 eg matching signature [(a,b)] against inferred type [(p,p)]
 451                 [then a and b will be unified together]
 452
 453         (c) not mentioned in the environment
 454                 eg the signature for f in this:
 455
 456                         g x = ... where
 457                                         f :: a->[a]
 458                                         f y = [x,y]
 459
 460                 Here, f is forced to be monorphic by the free occurence of x.
 461
 462 Before doing this, the substitution is applied to the signature type variable.
 463
 464 It's {\em assumed} that the substitution has already been applied to the
 465 environment type variables.
 466
 467 \begin{code}
 468 checkSigTyVars :: [TyVar]       -- Tyvars free in environment;
 469                                 -- fixed points of substitution
 470                -> [TyVar]       -- The original signature type variables
 471                -> UniType       -- signature type (for err msg)
 472                -> UniType       -- inferred type (for err msg)
 473                -> UnifyErrContext -- also for error msg
 474                -> TcM [TyVar]   -- Post-substitution signature type variables
 475
 476 checkSigTyVars env_tyvars sig_tyvars sig_tau inferred_tau err_ctxt
 477   = getSrcLocTc                                 `thenNF_Tc` \ locn ->
 478     applyTcSubstToTy inferred_tau               `thenNF_Tc` \ inferred_tau' ->
 479     let
 480         match_err = badMatchErr sig_tau inferred_tau' err_ctxt locn
 481     in
 482     applyTcSubstToTyVars sig_tyvars     `thenNF_Tc` \ sig_tys ->
 483
 484          -- Check point (a) above
 485     checkMaybesTc (map getTyVarMaybe sig_tys) match_err `thenTc` \ sig_tyvars' ->
 486
 487          -- Check point (b)
 488     checkTc (not (hasNoDups sig_tyvars')) match_err     `thenTc_`
 489
 490         -- Check point (c)
 491         -- We want to report errors in terms of the original signature tyvars,
 492         -- ie sig_tyvars, NOT sig_tyvars'.  sig_tys and sig_tyvars' correspond
 493         -- 1-1 with sig_tyvars, so we can just map back.
 494     let
 495         is_elem = isIn "checkSigTyVars"
 496
 497         mono_tyvars = [ sig_tyvar
 498                       | (sig_tyvar,sig_tyvar') <- zipEqual sig_tyvars sig_tyvars',
 499                         sig_tyvar' `is_elem` env_tyvars
 500                       ]
 501     in
 502     checkTc (not (null mono_tyvars))
 503             (notAsPolyAsSigErr sig_tau mono_tyvars err_ctxt locn) `thenTc_`
 504
 505     returnTc sig_tyvars'
 506 \end{code}