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          hiding ( rnMtoTcM )
  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,
  24                           newTyVarTy, zonkTcType
  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(..), TcIdBndr(..), TcHsBinds(..), TcBind(..), TcExpr(..), tcIdType )
  32
  33 import Bag              ( Bag, foldBag, bagToList, listToBag, isEmptyBag )
  34 import Class            ( GenClass )
  35 import Id               ( GenId, Id(..), mkUserId, idType )
  36 import Kind             ( isUnboxedKind, isTypeKind, mkBoxedTypeKind )
  37 import ListSetOps       ( minusList, unionLists, intersectLists )
  38 import Maybes           ( Maybe(..), 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_maybe, tyVarsOfTypes, eqSimpleTheta )
  45 import TyVar            ( GenTyVar, TyVar(..), tyVarKind, minusTyVarSet, emptyTyVarSet,
  46                           elementOfTyVarSet, unionTyVarSets, tyVarSetToList )
  47 import Usage            ( 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     in
 154
 155         -- DEAL WITH OVERLOADING
 156     resolveOverloading tyvars_to_gen lie bind sig_infos
 157                  `thenTc` \ (lie', reduced_tyvars_to_gen, dict_binds, dicts_bound) ->
 158
 159         -- Check for generaliseation over unboxed types, and
 160         -- default any TypeKind TyVars to BoxedTypeKind
 161     let
 162         tyvars = tyVarSetToList reduced_tyvars_to_gen   -- Commit to a particular order
 163
 164         unboxed_kind_tyvars    = filter (isUnboxedKind . tyVarKind) tyvars
 165         unresolved_kind_tyvars = filter (isTypeKind    . tyVarKind) tyvars
 166
 167         box_it tyvar = newTyVarTy mkBoxedTypeKind       `thenNF_Tc` \ boxed_ty ->
 168                        unifyTauTy (mkTyVarTy tyvar) boxed_ty
 169
 170     in
 171     ASSERT( null unboxed_kind_tyvars )  -- The instCantBeGeneralised stuff in tcSimplify
 172                                         -- should have dealt with unboxed type variables;
 173                                         -- and it's better done there because we have more
 174                                         -- precise origin information
 175
 176     mapTc box_it unresolved_kind_tyvars                 `thenTc_`
 177
 178          -- BUILD THE NEW LOCALS
 179     let
 180         dict_tys    = map tcIdType dicts_bound
 181         poly_tys    = map (mkForAllTys tyvars . mkFunTys dict_tys) mono_id_types
 182         poly_ids    = zipWithEqual "genspecetc" mk_poly binder_names poly_tys
 183         mk_poly name ty = mkUserId name ty (prag_info_fn name)
 184     in
 185          -- BUILD RESULTS
 186     returnTc (
 187          AbsBinds tyvars
 188                   dicts_bound
 189                   (zipEqual "genBinds" (map TcId mono_ids) (map TcId poly_ids))
 190                   dict_binds
 191                   bind,
 192          lie',
 193          poly_ids
 194     )
 195
 196 get_zonked_theta (TySigInfo _ _ theta _ _)
 197   = mapNF_Tc (\ (c,t) -> zonkTcType t `thenNF_Tc` \ t' -> returnNF_Tc (c,t')) theta
 198 \end{code}
 199
 200
 201 \begin{code}
 202 resolveOverloading
 203         :: TcTyVarSet s         -- Tyvars over which we are going to generalise
 204         -> LIE s                -- The LIE to deal with
 205         -> TcBind s             -- The binding group
 206         -> [TcSigInfo s]        -- And its real type-signature information
 207         -> TcM s (LIE s,                        -- LIE to pass up the way; a fixed point of
 208                                                 -- the current substitution
 209                   TcTyVarSet s,                 -- Revised tyvars to generalise
 210                   [(TcIdOcc s, TcExpr s)],      -- Dict bindings
 211                   [TcIdOcc s])                  -- List of dicts to bind here
 212
 213 resolveOverloading tyvars_to_gen dicts bind ty_sigs
 214   | not (isUnRestrictedGroup tysig_vars bind)
 215   =     -- Restricted group, so bind no dictionaries, and
 216         -- remove from tyvars_to_gen any constrained type variables
 217
 218         -- *Don't* simplify dicts at this point, because we aren't going
 219         -- to generalise over these dicts.  By the time we do simplify them
 220         -- we may well know more.  For example (this actually came up)
 221         --      f :: Array Int Int
 222         --      f x = array ... xs where xs = [1,2,3,4,5]
 223         -- We don't want to generate lots of (fromInt Int 1), (fromInt Int 2)
 224         -- stuff.  If we simplify only at the f-binding (not the xs-binding)
 225         -- we'll know that the literals are all Ints, and we can just produce
 226         -- Int literals!
 227
 228         -- Find all the type variables involved in overloading, the "constrained_tyvars"
 229         -- These are the ones we *aren't* going to generalise.
 230         -- We must be careful about doing this:
 231         --  (a) If we fail to generalise a tyvar which is not actually
 232         --      constrained, then it will never, ever get bound, and lands
 233         --      up printed out in interface files!  Notorious example:
 234         --              instance Eq a => Eq (Foo a b) where ..
 235         --      Here, b is not constrained, even though it looks as if it is.
 236         --      Another, more common, example is when there's a Method inst in
 237         --      the LIE, whose type might very well involve non-overloaded
 238         --      type variables.
 239         --  (b) On the other hand, we mustn't generalise tyvars which are constrained,
 240         --      because we are going to pass on out the unmodified LIE, with those
 241         --      tyvars in it.  They won't be in scope if we've generalised them.
 242         --
 243         -- So we are careful, and do a complete simplification just to find the
 244         -- constrained tyvars. We don't use any of the results, except to
 245         -- find which tyvars are constrained.
 246
 247         tcSimplify tyvars_to_gen dicts      `thenTc` \ (_, _, dicts_sig) ->
 248         let
 249           -- ASSERT: dicts_sig is already zonked!
 250           constrained_tyvars    = foldBag unionTyVarSets tyVarsOfInst emptyTyVarSet dicts_sig
 251           reduced_tyvars_to_gen = tyvars_to_gen `minusTyVarSet` constrained_tyvars
 252         in
 253
 254         -- Do it again, but with increased free_tyvars/reduced_tyvars_to_gen:
 255         -- We still need to do this simplification, because some dictionaries
 256         -- may gratuitouslyconstrain some tyvars over which we *are* going
 257         -- to generalise.
 258         -- For example d::Eq (Foo a b), where Foo is instanced as above.
 259         tcSimplifyWithExtraGlobals constrained_tyvars reduced_tyvars_to_gen dicts
 260                                     `thenTc` \ (dicts_free, dicts_binds, dicts_sig2) ->
 261         ASSERT(isEmptyBag dicts_sig2)
 262
 263         returnTc (dicts_free,                   -- All these are left unbound
 264                   reduced_tyvars_to_gen,
 265                   dicts_binds,                  -- Local dict binds
 266                   [])                           -- No lambda-bound dicts
 267
 268                 -- The returned LIE should be a fixed point of the substitution
 269
 270   | otherwise   -- An unrestricted group
 271   = case ty_sigs of
 272         [] ->   -- NO TYPE SIGNATURES
 273
 274             tcSimplify tyvars_to_gen dicts  `thenTc` \ (dicts_free, dict_binds, dicts_sig) ->
 275             returnTc (dicts_free, tyvars_to_gen, dict_binds,
 276                       map instToId (bagToList dicts_sig))
 277
 278         (TySigInfo _ _ theta _ _ : other) -> -- TYPE SIGNATURES PRESENT!
 279
 280             tcAddErrCtxt (sigsCtxt tysig_vars) $
 281
 282             newDicts SignatureOrigin theta      `thenNF_Tc` \ (dicts_sig, dict_ids) ->
 283
 284                     -- Check that the needed dicts can be expressed in
 285                     -- terms of the signature ones
 286             tcSimplifyAndCheck
 287                 tyvars_to_gen   -- Type vars over which we will quantify
 288                 dicts_sig       -- Available dicts
 289                 dicts           -- Want bindings for these dicts
 290
 291                                     `thenTc` \ (dicts_free, dict_binds) ->
 292
 293             returnTc (dicts_free, tyvars_to_gen, dict_binds, dict_ids)
 294   where
 295     tysig_vars   = [sig_var | (TySigInfo sig_var _ _ _ _) <- ty_sigs]
 296 \end{code}
 297
 298 @checkSigMatch@ does the next step in checking signature matching.
 299 The tau-type part has already been unified.  What we do here is to
 300 check that this unification has not over-constrained the (polymorphic)
 301 type variables of the original signature type.
 302
 303 The error message here is somewhat unsatisfactory, but it'll do for
 304 now (ToDo).
 305
 306 \begin{code}
 307 checkSigMatch :: TcSigInfo s -> TcM s ()
 308
 309 checkSigMatch (TySigInfo id sig_tyvars _ tau_ty src_loc)
 310   = tcAddSrcLoc src_loc $
 311     tcAddErrCtxt (sigCtxt id) $
 312     checkSigTyVars sig_tyvars tau_ty
 313 \end{code}
 314
 315
 316 %************************************************************************
 317 %*                                                                      *
 318 \subsection[GenEtc-monomorphism]{The monomorphism restriction}
 319 %*                                                                      *
 320 %************************************************************************
 321
 322 Not exported:
 323
 324 \begin{code}
 325 isUnRestrictedGroup :: [TcIdBndr s]             -- Signatures given for these
 326                     -> TcBind s
 327                     -> Bool
 328
 329 isUnRestrictedGroup sigs EmptyBind              = True
 330 isUnRestrictedGroup sigs (NonRecBind monobinds) = isUnResMono sigs monobinds
 331 isUnRestrictedGroup sigs (RecBind monobinds)    = isUnResMono sigs monobinds
 332
 333 is_elem v vs = isIn "isUnResMono" v vs
 334
 335 isUnResMono sigs (PatMonoBind (VarPat (TcId v)) _ _)    = v `is_elem` sigs
 336 isUnResMono sigs (PatMonoBind other      _ _)           = False
 337 isUnResMono sigs (VarMonoBind (TcId v) _)               = v `is_elem` sigs
 338 isUnResMono sigs (FunMonoBind _ _ _ _)                  = True
 339 isUnResMono sigs (AndMonoBinds mb1 mb2)                 = isUnResMono sigs mb1 &&
 340                                                           isUnResMono sigs mb2
 341 isUnResMono sigs EmptyMonoBinds                         = True
 342 \end{code}
 343
 344
 345 %************************************************************************
 346 %*                                                                      *
 347 \subsection[GenEtc-sig]{Matching a type signature}
 348 %*                                                                      *
 349 %************************************************************************
 350
 351 @checkSigTyVars@ is used after the type in a type signature has been unified with
 352 the actual type found.  It then checks that the type variables of the type signature
 353 are
 354         (a) still all type variables
 355                 eg matching signature [a] against inferred type [(p,q)]
 356                 [then a will be unified to a non-type variable]
 357
 358         (b) still all distinct
 359                 eg matching signature [(a,b)] against inferred type [(p,p)]
 360                 [then a and b will be unified together]
 361
 362 BUT ACTUALLY THESE FIRST TWO ARE FORCED BY USING DontBind TYVARS
 363
 364         (c) not mentioned in the environment
 365                 eg the signature for f in this:
 366
 367                         g x = ... where
 368                                         f :: a->[a]
 369                                         f y = [x,y]
 370
 371                 Here, f is forced to be monorphic by the free occurence of x.
 372
 373 Before doing this, the substitution is applied to the signature type variable.
 374
 375 \begin{code}
 376 checkSigTyVars :: [TcTyVar s]           -- The original signature type variables
 377                -> TcType s              -- signature type (for err msg)
 378                -> TcM s ()
 379
 380 checkSigTyVars sig_tyvars sig_tau
 381   = tcGetGlobalTyVars                   `thenNF_Tc` \ env_tyvars ->
 382     checkSigTyVarsGivenGlobals env_tyvars sig_tyvars sig_tau
 383
 384 checkSigTyVarsGivenGlobals
 385          :: TcTyVarSet s        -- Consider these fully-zonked tyvars as global
 386          -> [TcTyVar s]         -- The original signature type variables
 387          -> TcType s            -- signature type (for err msg)
 388          -> TcM s ()
 389
 390 checkSigTyVarsGivenGlobals globals sig_tyvars sig_tau
 391   =     -- Check point (c)
 392         -- We want to report errors in terms of the original signature tyvars,
 393         -- ie sig_tyvars, NOT sig_tyvars'.  sig_tys and sig_tyvars' correspond
 394         -- 1-1 with sig_tyvars, so we can just map back.
 395     checkTc (null mono_tyvars)
 396             (notAsPolyAsSigErr sig_tau mono_tyvars)
 397   where
 398     mono_tyvars = filter (`elementOfTyVarSet` globals) sig_tyvars
 399 \end{code}
 400
 401
 402
 403
 404 Contexts and errors
 405 ~~~~~~~~~~~~~~~~~~~
 406 \begin{code}
 407 notAsPolyAsSigErr sig_tau mono_tyvars sty
 408   = ppHang (ppStr "A type signature is more polymorphic than the inferred type")
 409         4  (ppAboves [ppStr "(That is, one or more type variables in the inferred type can't be forall'd.)",
 410                       ppHang (ppStr "Monomorphic type variable(s):")
 411                            4 (interpp'SP sty mono_tyvars),
 412                       ppStr "Possible cause: the RHS mentions something subject to the monomorphism restriction"
 413                      ])
 414 \end{code}
 415
 416
 417 \begin{code}
 418 badMatchErr sig_ty inferred_ty sty
 419   = ppHang (ppStr "Type signature doesn't match inferred type")
 420          4 (ppAboves [ppHang (ppStr "Signature:") 4 (ppr sty sig_ty),
 421                       ppHang (ppStr "Inferred :") 4 (ppr sty inferred_ty)
 422            ])
 423
 424 sigCtxt id sty
 425   = ppSep [ppStr "When checking signature for", ppr sty id]
 426 sigsCtxt ids sty
 427   = ppSep [ppStr "When checking signature(s) for:", interpp'SP sty ids]
 428 \end{code}
 429
 430
 431 \begin{code}
 432 sigContextsErr ty_sigs sty
 433   = ppHang (ppStr "A group of type signatures have mismatched contexts")
 434          4 (ppAboves (map ppr_sig_info ty_sigs))
 435   where
 436     ppr_sig_info (TySigInfo val tyvars theta tau_ty _)
 437       = ppHang (ppBeside (ppr sty val) (ppStr " :: "))
 438              4 (if null theta
 439                 then ppNil
 440                 else ppBesides [ppStr "(",
 441                                 ppIntersperse (ppStr ", ") (map (ppr_inst sty) theta),
 442                                 ppStr ") => ..."])
 443     ppr_inst sty (clas, ty) = ppCat [ppr sty clas, ppr sty ty]
 444 \end{code}