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