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