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