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