ghc/compiler/typecheck/TcType.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[TcType]{Types used in the typechecker}
   5
   6 This module provides the Type interface for front-end parts of the
   7 compiler.  These parts
   8
   9         * treat "source types" as opaque:
  10                 newtypes, and predicates are meaningful.
  11         * look through usage types
  12
  13 The "tc" prefix is for "typechechecker", because the type checker
  14 is the principal client.
  15
  16 \begin{code}
  17 module TcType (
  18   --------------------------------
  19   -- Types
  20   TcType, TcSigmaType, TcPhiType, TcTauType, TcPredType, TcThetaType,
  21   TcTyVar, TcTyVarSet, TcKind,
  22
  23   --------------------------------
  24   -- TyVarDetails
  25   TyVarDetails(..), isUserTyVar, isSkolemTyVar, isHoleTyVar,
  26   tyVarBindingInfo,
  27
  28   --------------------------------
  29   -- Builders
  30   mkRhoTy, mkSigmaTy,
  31
  32   --------------------------------
  33   -- Splitters
  34   -- These are important because they do not look through newtypes
  35   tcSplitForAllTys, tcSplitRhoTy,
  36   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
  37   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
  38   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy,
  39   tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
  40
  41   ---------------------------------
  42   -- Predicates.
  43   -- Again, newtypes are opaque
  44   tcEqType, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
  45   isSigmaTy, isOverloadedTy,
  46   isDoubleTy, isFloatTy, isIntTy,
  47   isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy,
  48   isTauTy, tcIsTyVarTy, tcIsForAllTy,
  49
  50   ---------------------------------
  51   -- Misc type manipulators
  52   hoistForAllTys, deNoteType,
  53   namesOfType, namesOfDFunHead,
  54   getDFunTyKey,
  55
  56   ---------------------------------
  57   -- Predicate types
  58   PredType, getClassPredTys_maybe, getClassPredTys,
  59   isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
  60   mkDictTy, tcSplitPredTy_maybe, predTyUnique,
  61   isDictTy, tcSplitDFunTy, predTyUnique,
  62   mkClassPred, inheritablePred, isIPPred, mkPredName,
  63
  64   ---------------------------------
  65   -- Foreign import and export
  66   isFFIArgumentTy,     -- :: DynFlags -> Safety -> Type -> Bool
  67   isFFIImportResultTy, -- :: DynFlags -> Type -> Bool
  68   isFFIExportResultTy, -- :: Type -> Bool
  69   isFFIExternalTy,     -- :: Type -> Bool
  70   isFFIDynArgumentTy,  -- :: Type -> Bool
  71   isFFIDynResultTy,    -- :: Type -> Bool
  72   isFFILabelTy,        -- :: Type -> Bool
  73
  74   ---------------------------------
  75   -- Unifier and matcher
  76   unifyTysX, unifyTyListsX, unifyExtendTysX,
  77   allDistinctTyVars,
  78   matchTy, matchTys, match,
  79
  80   --------------------------------
  81   -- Rexported from Type
  82   Kind,         -- Stuff to do with kinds is insensitive to pre/post Tc
  83   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
  84   superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
  85   isTypeKind,
  86
  87   IPName, ipNameName, mapIPName,
  88
  89   Type, SourceType(..), PredType, ThetaType,
  90   mkForAllTy, mkForAllTys,
  91   mkFunTy, mkFunTys, zipFunTys,
  92   mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
  93   mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
  94
  95   isUnLiftedType,       -- Source types are always lifted
  96   isUnboxedTupleType,   -- Ditto
  97   isPrimitiveType,
  98
  99   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
 100   tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars,
 101   typeKind, eqKind, eqUsage,
 102
 103   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
 104   ) where
 105
 106 #include "HsVersions.h"
 107
 108
 109 import {-# SOURCE #-} PprType( pprType )
 110
 111 -- friends:
 112 import TypeRep          ( Type(..), TyNote(..), funTyCon )  -- friend
 113 import Type             ( mkUTyM, unUTy )       -- Used locally
 114
 115 import Type             (       -- Re-exports
 116                           tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
 117                           IPName, Kind, Type, SourceType(..), PredType, ThetaType,
 118                           unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
 119                           mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
 120                           mkFunTy, mkFunTys, zipFunTys,
 121                           mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
 122                           mkTyVarTy, mkTyVarTys, mkTyConTy, mkPredTy, mkPredTys,
 123                           isUnLiftedType, isUnboxedTupleType, isPrimitiveType,
 124                           splitNewType_maybe, splitTyConApp_maybe,
 125                           tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
 126                           tidyTyVarBndr, tidyOpenTyVar, tidyOpenTyVars, eqKind, eqUsage,
 127                           hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind,
 128                           ipNameName, mapIPName
 129                         )
 130 import TyCon            ( TyCon, isUnLiftedTyCon )
 131 import Class            ( classHasFDs, Class )
 132 import Var              ( TyVar, tyVarKind, isMutTyVar, mutTyVarDetails )
 133 import ForeignCall      ( Safety, playSafe )
 134 import VarEnv
 135 import VarSet
 136
 137 -- others:
 138 import CmdLineOpts      ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
 139 import Name             ( Name, NamedThing(..), mkLocalName, getSrcLoc )
 140 import OccName          ( OccName, mkDictOcc )
 141 import NameSet
 142 import PrelNames        -- Lots (e.g. in isFFIArgumentTy)
 143 import TysWiredIn       ( ptrTyCon, funPtrTyCon, addrTyCon, unitTyCon )
 144 import Unique           ( Unique, Uniquable(..) )
 145 import SrcLoc           ( SrcLoc )
 146 import Util             ( cmpList, thenCmp, equalLength )
 147 import Maybes           ( maybeToBool, expectJust )
 148 import Outputable
 149 \end{code}
 150
 151
 152 %************************************************************************
 153 %*                                                                      *
 154 \subsection{Types}
 155 %*                                                                      *
 156 %************************************************************************
 157
 158 The type checker divides the generic Type world into the
 159 following more structured beasts:
 160
 161 sigma ::= forall tyvars. theta => phi
 162         -- A sigma type is a qualified type
 163         --
 164         -- Note that even if 'tyvars' is empty, theta
 165         -- may not be: e.g.   (?x::Int) => Int
 166
 167         -- Note that 'sigma' is in prenex form:
 168         -- all the foralls are at the front.
 169         -- A 'phi' type has no foralls to the right of
 170         -- an arrow
 171
 172 phi ::= sigma -> phi
 173      |  tau
 174
 175 -- A 'tau' type has no quantification anywhere
 176 -- Note that the args of a type constructor must be taus
 177 tau ::= tyvar
 178      |  tycon tau_1 .. tau_n
 179      |  tau_1 tau_2
 180      |  tau_1 -> tau_2
 181
 182 -- In all cases, a (saturated) type synonym application is legal,
 183 -- provided it expands to the required form.
 184
 185
 186 \begin{code}
 187 type SigmaType = Type
 188 type PhiType   = Type
 189 type TauType   = Type
 190 \end{code}
 191
 192 \begin{code}
 193 type TcTyVar    = TyVar         -- Might be a mutable tyvar
 194 type TcTyVarSet = TyVarSet
 195
 196 type TcType = Type              -- A TcType can have mutable type variables
 197         -- Invariant on ForAllTy in TcTypes:
 198         --      forall a. T
 199         -- a cannot occur inside a MutTyVar in T; that is,
 200         -- T is "flattened" before quantifying over a
 201
 202 type TcPredType     = PredType
 203 type TcThetaType    = ThetaType
 204 type TcSigmaType    = TcType
 205 type TcPhiType      = TcType
 206 type TcTauType      = TcType
 207 type TcKind         = TcType
 208 \end{code}
 209
 210
 211 %************************************************************************
 212 %*                                                                      *
 213 \subsection{TyVarDetails}
 214 %*                                                                      *
 215 %************************************************************************
 216
 217 TyVarDetails gives extra info about type variables, used during type
 218 checking.  It's attached to mutable type variables only.
 219 It's knot-tied back to Var.lhs.  There is no reason in principle
 220 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
 221
 222 \begin{code}
 223 data TyVarDetails
 224   = HoleTv      -- Used *only* by the type checker when passing in a type
 225                 -- variable that should be side-effected to the result type.
 226                 -- Always has kind openTypeKind.
 227                 -- Never appears in types
 228
 229   | SigTv       -- Introduced when instantiating a type signature,
 230                 -- prior to checking that the defn of a fn does
 231                 -- have the expected type.  Should not be instantiated.
 232                 --
 233                 --      f :: forall a. a -> a
 234                 --      f = e
 235                 -- When checking e, with expected type (a->a), we
 236                 -- should not instantiate a
 237
 238    | ClsTv      -- Scoped type variable introduced by a class decl
 239                 --      class C a where ...
 240
 241    | InstTv     -- Ditto, but instance decl
 242
 243    | PatSigTv   -- Scoped type variable, introduced by a pattern
 244                 -- type signature
 245                 --      \ x::a -> e
 246
 247    | VanillaTv  -- Everything else
 248
 249 isUserTyVar :: TcTyVar -> Bool  -- Avoid unifying these if possible
 250 isUserTyVar tv = case mutTyVarDetails tv of
 251                    VanillaTv -> False
 252                    other     -> True
 253
 254 isSkolemTyVar :: TcTyVar -> Bool
 255 isSkolemTyVar tv = case mutTyVarDetails tv of
 256                       SigTv -> True
 257                       oteher -> False
 258
 259 isHoleTyVar :: TcTyVar -> Bool
 260 -- NB:  the hole might be filled in by now, and this
 261 --      function does not check for that
 262 isHoleTyVar tv = ASSERT( isMutTyVar tv )
 263                  case mutTyVarDetails tv of
 264                         HoleTv -> True
 265                         other  -> False
 266
 267 tyVarBindingInfo :: TyVar -> SDoc       -- Used in checkSigTyVars
 268 tyVarBindingInfo tv
 269   | isMutTyVar tv
 270   = sep [ptext SLIT("is bound by the") <+> details (mutTyVarDetails tv),
 271          ptext SLIT("at") <+> ppr (getSrcLoc tv)]
 272   | otherwise
 273   = empty
 274   where
 275     details SigTv     = ptext SLIT("type signature")
 276     details ClsTv     = ptext SLIT("class declaration")
 277     details InstTv    = ptext SLIT("instance declaration")
 278     details PatSigTv  = ptext SLIT("pattern type signature")
 279     details HoleTv    = ptext SLIT("//hole//")          -- Should not happen
 280     details VanillaTv = ptext SLIT("//vanilla//")       -- Ditto
 281 \end{code}
 282
 283
 284 %************************************************************************
 285 %*                                                                      *
 286 \subsection{Tau, sigma and rho}
 287 %*                                                                      *
 288 %************************************************************************
 289
 290 \begin{code}
 291 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
 292
 293 mkRhoTy :: [SourceType] -> Type -> Type
 294 mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty )
 295                    foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta
 296
 297 \end{code}
 298
 299
 300 @isTauTy@ tests for nested for-alls.
 301
 302 \begin{code}
 303 isTauTy :: Type -> Bool
 304 isTauTy (TyVarTy v)      = True
 305 isTauTy (TyConApp _ tys) = all isTauTy tys
 306 isTauTy (AppTy a b)      = isTauTy a && isTauTy b
 307 isTauTy (FunTy a b)      = isTauTy a && isTauTy b
 308 isTauTy (SourceTy p)     = True         -- Don't look through source types
 309 isTauTy (NoteTy _ ty)    = isTauTy ty
 310 isTauTy (UsageTy _ ty)   = isTauTy ty
 311 isTauTy other            = False
 312 \end{code}
 313
 314 \begin{code}
 315 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
 316                                 -- construct a dictionary function name
 317 getDFunTyKey (TyVarTy tv)            = getOccName tv
 318 getDFunTyKey (TyConApp tc _)         = getOccName tc
 319 getDFunTyKey (AppTy fun _)           = getDFunTyKey fun
 320 getDFunTyKey (NoteTy _ t)            = getDFunTyKey t
 321 getDFunTyKey (FunTy arg _)           = getOccName funTyCon
 322 getDFunTyKey (ForAllTy _ t)          = getDFunTyKey t
 323 getDFunTyKey (UsageTy _ t)           = getDFunTyKey t
 324 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc    -- Newtypes are quite reasonable
 325 getDFunTyKey ty                      = pprPanic "getDFunTyKey" (pprType ty)
 326 -- SourceTy shouldn't happen
 327 \end{code}
 328
 329
 330 %************************************************************************
 331 %*                                                                      *
 332 \subsection{Expanding and splitting}
 333 %*                                                                      *
 334 %************************************************************************
 335
 336 These tcSplit functions are like their non-Tc analogues, but
 337         a) they do not look through newtypes
 338         b) they do not look through PredTys
 339         c) [future] they ignore usage-type annotations
 340
 341 However, they are non-monadic and do not follow through mutable type
 342 variables.  It's up to you to make sure this doesn't matter.
 343
 344 \begin{code}
 345 tcSplitForAllTys :: Type -> ([TyVar], Type)
 346 tcSplitForAllTys ty = split ty ty []
 347    where
 348      split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
 349      split orig_ty (NoteTy n  ty)   tvs = split orig_ty ty tvs
 350      split orig_ty (UsageTy _ ty)   tvs = split orig_ty ty tvs
 351      split orig_ty t                tvs = (reverse tvs, orig_ty)
 352
 353 tcIsForAllTy (ForAllTy tv ty) = True
 354 tcIsForAllTy (NoteTy n ty)    = tcIsForAllTy ty
 355 tcIsForAllTy (UsageTy n ty)   = tcIsForAllTy ty
 356 tcIsForAllTy t                = False
 357
 358 tcSplitRhoTy :: Type -> ([PredType], Type)
 359 tcSplitRhoTy ty = split ty ty []
 360  where
 361   split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
 362                                         Just p  -> split res res (p:ts)
 363                                         Nothing -> (reverse ts, orig_ty)
 364   split orig_ty (NoteTy n ty)   ts = split orig_ty ty ts
 365   split orig_ty (UsageTy _ ty)  ts = split orig_ty ty ts
 366   split orig_ty ty              ts = (reverse ts, orig_ty)
 367
 368 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
 369                         (tvs, rho) -> case tcSplitRhoTy rho of
 370                                         (theta, tau) -> (tvs, theta, tau)
 371
 372 tcTyConAppTyCon :: Type -> TyCon
 373 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
 374
 375 tcTyConAppArgs :: Type -> [Type]
 376 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
 377
 378 tcSplitTyConApp :: Type -> (TyCon, [Type])
 379 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
 380                         Just stuff -> stuff
 381                         Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 382
 383 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
 384 -- Newtypes are opaque, so they may be split
 385 tcSplitTyConApp_maybe (TyConApp tc tys)         = Just (tc, tys)
 386 tcSplitTyConApp_maybe (FunTy arg res)           = Just (funTyCon, [unUTy arg,unUTy res])
 387 tcSplitTyConApp_maybe (NoteTy n ty)             = tcSplitTyConApp_maybe ty
 388 tcSplitTyConApp_maybe (UsageTy _ ty)            = tcSplitTyConApp_maybe ty
 389 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
 390         -- However, predicates are not treated
 391         -- as tycon applications by the type checker
 392 tcSplitTyConApp_maybe other                     = Nothing
 393
 394 tcSplitFunTys :: Type -> ([Type], Type)
 395 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
 396                         Nothing        -> ([], ty)
 397                         Just (arg,res) -> (arg:args, res')
 398                                        where
 399                                           (args,res') = tcSplitFunTys res
 400
 401 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
 402 tcSplitFunTy_maybe (FunTy arg res)  = Just (arg, res)
 403 tcSplitFunTy_maybe (NoteTy n ty)    = tcSplitFunTy_maybe ty
 404 tcSplitFunTy_maybe (UsageTy _ ty)   = tcSplitFunTy_maybe ty
 405 tcSplitFunTy_maybe other            = Nothing
 406
 407 tcFunArgTy    ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
 408 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
 409
 410
 411 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
 412 tcSplitAppTy_maybe (FunTy ty1 ty2)           = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
 413 tcSplitAppTy_maybe (AppTy ty1 ty2)           = Just (ty1, ty2)
 414 tcSplitAppTy_maybe (NoteTy n ty)             = tcSplitAppTy_maybe ty
 415 tcSplitAppTy_maybe (UsageTy _ ty)            = tcSplitAppTy_maybe ty
 416 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
 417         --- Don't forget that newtype!
 418 tcSplitAppTy_maybe (TyConApp tc tys)         = tc_split_app tc tys
 419 tcSplitAppTy_maybe other                     = Nothing
 420
 421 tc_split_app tc []  = Nothing
 422 tc_split_app tc tys = split tys []
 423                     where
 424                       split [ty2]    acc = Just (TyConApp tc (reverse acc), ty2)
 425                       split (ty:tys) acc = split tys (ty:acc)
 426
 427 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
 428                     Just stuff -> stuff
 429                     Nothing    -> pprPanic "tcSplitAppTy" (pprType ty)
 430
 431 tcGetTyVar_maybe :: Type -> Maybe TyVar
 432 tcGetTyVar_maybe (TyVarTy tv)   = Just tv
 433 tcGetTyVar_maybe (NoteTy _ t)   = tcGetTyVar_maybe t
 434 tcGetTyVar_maybe ty@(UsageTy _ _) = pprPanic "tcGetTyVar_maybe: UTy:" (pprType ty)
 435 tcGetTyVar_maybe other          = Nothing
 436
 437 tcGetTyVar :: String -> Type -> TyVar
 438 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
 439
 440 tcIsTyVarTy :: Type -> Bool
 441 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
 442 \end{code}
 443
 444 The type of a method for class C is always of the form:
 445         Forall a1..an. C a1..an => sig_ty
 446 where sig_ty is the type given by the method's signature, and thus in general
 447 is a ForallTy.  At the point that splitMethodTy is called, it is expected
 448 that the outer Forall has already been stripped off.  splitMethodTy then
 449 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
 450 Usages stripped off.
 451
 452 \begin{code}
 453 tcSplitMethodTy :: Type -> (PredType, Type)
 454 tcSplitMethodTy ty = split ty
 455  where
 456   split (FunTy arg res) = case tcSplitPredTy_maybe arg of
 457                             Just p  -> (p, res)
 458                             Nothing -> panic "splitMethodTy"
 459   split (NoteTy n ty)   = split ty
 460   split (UsageTy _ ty)  = split ty
 461   split _               = panic "splitMethodTy"
 462
 463 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
 464 -- Split the type of a dictionary function
 465 tcSplitDFunTy ty
 466   = case tcSplitSigmaTy ty       of { (tvs, theta, tau) ->
 467     case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
 468     (tvs, theta, clas, tys) }}
 469 \end{code}
 470
 471
 472 %************************************************************************
 473 %*                                                                      *
 474 \subsection{Predicate types}
 475 %*                                                                      *
 476 %************************************************************************
 477
 478 "Predicates" are particular source types, namelyClassP or IParams
 479
 480 \begin{code}
 481 isPred :: SourceType -> Bool
 482 isPred (ClassP _ _) = True
 483 isPred (IParam _ _) = True
 484 isPred (NType _ _)  = False
 485
 486 isPredTy :: Type -> Bool
 487 isPredTy (NoteTy _ ty)  = isPredTy ty
 488 isPredTy (UsageTy _ ty) = isPredTy ty
 489 isPredTy (SourceTy sty) = isPred sty
 490 isPredTy _              = False
 491
 492 tcSplitPredTy_maybe :: Type -> Maybe PredType
 493    -- Returns Just for predicates only
 494 tcSplitPredTy_maybe (NoteTy _ ty)           = tcSplitPredTy_maybe ty
 495 tcSplitPredTy_maybe (UsageTy _ ty)          = tcSplitPredTy_maybe ty
 496 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
 497 tcSplitPredTy_maybe other                   = Nothing
 498
 499 predTyUnique :: PredType -> Unique
 500 predTyUnique (IParam n _)      = getUnique (ipNameName n)
 501 predTyUnique (ClassP clas tys) = getUnique clas
 502
 503 predHasFDs :: PredType -> Bool
 504 -- True if the predicate has functional depenencies;
 505 -- I.e. should participate in improvement
 506 predHasFDs (IParam _ _)   = True
 507 predHasFDs (ClassP cls _) = classHasFDs cls
 508
 509 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
 510 mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
 511 mkPredName uniq loc (IParam ip ty)   = mkLocalName uniq (getOccName (ipNameName ip)) loc
 512 \end{code}
 513
 514
 515 --------------------- Dictionary types ---------------------------------
 516
 517 \begin{code}
 518 mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
 519                        ClassP clas tys
 520
 521 isClassPred :: SourceType -> Bool
 522 isClassPred (ClassP clas tys) = True
 523 isClassPred other             = False
 524
 525 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
 526 isTyVarClassPred other             = False
 527
 528 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
 529 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
 530 getClassPredTys_maybe _                 = Nothing
 531
 532 getClassPredTys :: PredType -> (Class, [Type])
 533 getClassPredTys (ClassP clas tys) = (clas, tys)
 534
 535 mkDictTy :: Class -> [Type] -> Type
 536 mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
 537                     mkPredTy (ClassP clas tys)
 538
 539 isDictTy :: Type -> Bool
 540 isDictTy (SourceTy p)   = isClassPred p
 541 isDictTy (NoteTy _ ty)  = isDictTy ty
 542 isDictTy (UsageTy _ ty) = isDictTy ty
 543 isDictTy other          = False
 544 \end{code}
 545
 546 --------------------- Implicit parameters ---------------------------------
 547
 548 \begin{code}
 549 isIPPred :: SourceType -> Bool
 550 isIPPred (IParam _ _) = True
 551 isIPPred other        = False
 552
 553 inheritablePred :: PredType -> Bool
 554 -- Can be inherited by a context.  For example, consider
 555 --      f x = let g y = (?v, y+x)
 556 --            in (g 3 with ?v = 8,
 557 --                g 4 with ?v = 9)
 558 -- The point is that g's type must be quantifed over ?v:
 559 --      g :: (?v :: a) => a -> a
 560 -- but it doesn't need to be quantified over the Num a dictionary
 561 -- which can be free in g's rhs, and shared by both calls to g
 562 inheritablePred (ClassP _ _) = True
 563 inheritablePred other        = False
 564 \end{code}
 565
 566
 567 %************************************************************************
 568 %*                                                                      *
 569 \subsection{Comparison}
 570 %*                                                                      *
 571 %************************************************************************
 572
 573 Comparison, taking note of newtypes, predicates, etc,
 574 But ignoring usage types
 575
 576 \begin{code}
 577 tcEqType :: Type -> Type -> Bool
 578 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
 579
 580 tcEqPred :: PredType -> PredType -> Bool
 581 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
 582
 583 -------------
 584 tcCmpType :: Type -> Type -> Ordering
 585 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
 586
 587 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
 588
 589 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
 590 -------------
 591 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
 592
 593 -------------
 594 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
 595   -- The "env" maps type variables in ty1 to type variables in ty2
 596   -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
 597   -- we in effect substitute tv2 for tv1 in t1 before continuing
 598
 599     -- Look through NoteTy and UsageTy
 600 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
 601 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
 602 cmpTy env (UsageTy _ ty1) ty2 = cmpTy env ty1 ty2
 603 cmpTy env ty1 (UsageTy _ ty2) = cmpTy env ty1 ty2
 604
 605     -- Deal with equal constructors
 606 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
 607                                           Just tv1a -> tv1a `compare` tv2
 608                                           Nothing   -> tv1  `compare` tv2
 609
 610 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
 611 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
 612 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
 613 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
 614 cmpTy env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTy (extendVarEnv env tv1 tv2) t1 t2
 615
 616     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
 617 cmpTy env (AppTy _ _) (TyVarTy _) = GT
 618
 619 cmpTy env (FunTy _ _) (TyVarTy _) = GT
 620 cmpTy env (FunTy _ _) (AppTy _ _) = GT
 621
 622 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
 623 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
 624 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
 625
 626 cmpTy env (ForAllTy _ _) (TyVarTy _)    = GT
 627 cmpTy env (ForAllTy _ _) (AppTy _ _)    = GT
 628 cmpTy env (ForAllTy _ _) (FunTy _ _)    = GT
 629 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
 630
 631 cmpTy env (SourceTy _)   t2             = GT
 632
 633 cmpTy env _ _ = LT
 634 \end{code}
 635
 636 \begin{code}
 637 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
 638 cmpSourceTy env (IParam n1 ty1) (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
 639         -- Compare types as well as names for implicit parameters
 640         -- This comparison is used exclusively (I think) for the
 641         -- finite map built in TcSimplify
 642 cmpSourceTy env (IParam _ _)     sty              = LT
 643
 644 cmpSourceTy env (ClassP _ _)     (IParam _ _)     = GT
 645 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
 646 cmpSourceTy env (ClassP _ _)     (NType _ _)      = LT
 647
 648 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
 649 cmpSourceTy env (NType _ _)      sty              = GT
 650 \end{code}
 651
 652 PredTypes are used as a FM key in TcSimplify,
 653 so we take the easy path and make them an instance of Ord
 654
 655 \begin{code}
 656 instance Eq  SourceType where { (==)    = tcEqPred }
 657 instance Ord SourceType where { compare = tcCmpPred }
 658 \end{code}
 659
 660
 661 %************************************************************************
 662 %*                                                                      *
 663 \subsection{Predicates}
 664 %*                                                                      *
 665 %************************************************************************
 666
 667 isSigmaTy returns true of any qualified type.  It doesn't *necessarily* have
 668 any foralls.  E.g.
 669         f :: (?x::Int) => Int -> Int
 670
 671 \begin{code}
 672 isSigmaTy :: Type -> Bool
 673 isSigmaTy (ForAllTy tyvar ty) = True
 674 isSigmaTy (FunTy a b)         = isPredTy a
 675 isSigmaTy (NoteTy n ty)       = isSigmaTy ty
 676 isSigmaTy (UsageTy _ ty)      = isSigmaTy ty
 677 isSigmaTy _                   = False
 678
 679 isOverloadedTy :: Type -> Bool
 680 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
 681 isOverloadedTy (FunTy a b)         = isPredTy a
 682 isOverloadedTy (NoteTy n ty)       = isOverloadedTy ty
 683 isOverloadedTy (UsageTy _ ty)      = isOverloadedTy ty
 684 isOverloadedTy _                   = False
 685 \end{code}
 686
 687 \begin{code}
 688 isFloatTy      = is_tc floatTyConKey
 689 isDoubleTy     = is_tc doubleTyConKey
 690 isForeignPtrTy = is_tc foreignPtrTyConKey
 691 isIntegerTy    = is_tc integerTyConKey
 692 isIntTy        = is_tc intTyConKey
 693 isAddrTy       = is_tc addrTyConKey
 694 isBoolTy       = is_tc boolTyConKey
 695 isUnitTy       = is_tc unitTyConKey
 696
 697 is_tc :: Unique -> Type -> Bool
 698 -- Newtypes are opaque to this
 699 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
 700                         Just (tc, _) -> uniq == getUnique tc
 701                         Nothing      -> False
 702 \end{code}
 703
 704
 705 %************************************************************************
 706 %*                                                                      *
 707 \subsection{Misc}
 708 %*                                                                      *
 709 %************************************************************************
 710
 711 \begin{code}
 712 hoistForAllTys :: Type -> Type
 713         -- Move all the foralls to the top
 714         -- e.g.  T -> forall a. a  ==>   forall a. T -> a
 715         -- Careful: LOSES USAGE ANNOTATIONS!
 716 hoistForAllTys ty
 717   = case hoist ty of { (tvs, body) -> mkForAllTys tvs body }
 718   where
 719     hoist :: Type -> ([TyVar], Type)
 720     hoist ty = case tcSplitFunTys    ty  of { (args, res) ->
 721                case tcSplitForAllTys res of {
 722                   ([], body)  -> ([], ty) ;
 723                   (tvs1, body1) -> case hoist body1 of { (tvs2,body2) ->
 724                                    (tvs1 ++ tvs2, mkFunTys args body2)
 725                }}}
 726 \end{code}
 727
 728
 729 \begin{code}
 730 deNoteType :: Type -> Type
 731         -- Remove synonyms, but not source types
 732 deNoteType ty@(TyVarTy tyvar)   = ty
 733 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
 734 deNoteType (SourceTy p)         = SourceTy (deNoteSourceType p)
 735 deNoteType (NoteTy _ ty)        = deNoteType ty
 736 deNoteType (AppTy fun arg)      = AppTy (deNoteType fun) (deNoteType arg)
 737 deNoteType (FunTy fun arg)      = FunTy (deNoteType fun) (deNoteType arg)
 738 deNoteType (ForAllTy tv ty)     = ForAllTy tv (deNoteType ty)
 739 deNoteType (UsageTy u ty)       = UsageTy u (deNoteType ty)
 740
 741 deNoteSourceType :: SourceType -> SourceType
 742 deNoteSourceType (ClassP c tys)   = ClassP c (map deNoteType tys)
 743 deNoteSourceType (IParam n ty)    = IParam n (deNoteType ty)
 744 deNoteSourceType (NType tc tys)   = NType tc (map deNoteType tys)
 745 \end{code}
 746
 747 Find the free names of a type, including the type constructors and classes it mentions
 748 This is used in the front end of the compiler
 749
 750 \begin{code}
 751 namesOfType :: Type -> NameSet
 752 namesOfType (TyVarTy tv)                = unitNameSet (getName tv)
 753 namesOfType (TyConApp tycon tys)        = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
 754 namesOfType (NoteTy (SynNote ty1) ty2)  = namesOfType ty1
 755 namesOfType (NoteTy other_note    ty2)  = namesOfType ty2
 756 namesOfType (SourceTy (IParam n ty))    = namesOfType ty
 757 namesOfType (SourceTy (ClassP cl tys))  = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
 758 namesOfType (SourceTy (NType tc tys))   = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
 759 namesOfType (FunTy arg res)             = namesOfType arg `unionNameSets` namesOfType res
 760 namesOfType (AppTy fun arg)             = namesOfType fun `unionNameSets` namesOfType arg
 761 namesOfType (ForAllTy tyvar ty)         = namesOfType ty `delFromNameSet` getName tyvar
 762 namesOfType (UsageTy u ty)              = namesOfType u `unionNameSets` namesOfType ty
 763
 764 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
 765
 766 namesOfDFunHead :: Type -> NameSet
 767 -- Find the free type constructors and classes
 768 -- of the head of the dfun instance type
 769 -- The 'dfun_head_type' is because of
 770 --      instance Foo a => Baz T where ...
 771 -- The decl is an orphan if Baz and T are both not locally defined,
 772 --      even if Foo *is* locally defined
 773 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
 774                                 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
 775                                                                       (map getName tvs)
 776 \end{code}
 777
 778
 779 %************************************************************************
 780 %*                                                                      *
 781 \subsection[TysWiredIn-ext-type]{External types}
 782 %*                                                                      *
 783 %************************************************************************
 784
 785 The compiler's foreign function interface supports the passing of a
 786 restricted set of types as arguments and results (the restricting factor
 787 being the )
 788
 789 \begin{code}
 790 isFFIArgumentTy :: DynFlags -> Safety -> Type -> Bool
 791 -- Checks for valid argument type for a 'foreign import'
 792 isFFIArgumentTy dflags safety ty
 793    = checkRepTyCon (legalOutgoingTyCon dflags safety) ty
 794
 795 isFFIExternalTy :: Type -> Bool
 796 -- Types that are allowed as arguments of a 'foreign export'
 797 isFFIExternalTy ty = checkRepTyCon legalFEArgTyCon ty
 798
 799 isFFIImportResultTy :: DynFlags -> Type -> Bool
 800 isFFIImportResultTy dflags ty
 801   = checkRepTyCon (legalFIResultTyCon dflags) ty
 802
 803 isFFIExportResultTy :: Type -> Bool
 804 isFFIExportResultTy ty = checkRepTyCon legalFEResultTyCon ty
 805
 806 isFFIDynArgumentTy :: Type -> Bool
 807 -- The argument type of a foreign import dynamic must be Ptr, FunPtr, Addr,
 808 -- or a newtype of either.
 809 isFFIDynArgumentTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
 810
 811 isFFIDynResultTy :: Type -> Bool
 812 -- The result type of a foreign export dynamic must be Ptr, FunPtr, Addr,
 813 -- or a newtype of either.
 814 isFFIDynResultTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
 815
 816 isFFILabelTy :: Type -> Bool
 817 -- The type of a foreign label must be Ptr, FunPtr, Addr,
 818 -- or a newtype of either.
 819 isFFILabelTy = checkRepTyCon (\tc -> tc == ptrTyCon || tc == funPtrTyCon || tc == addrTyCon)
 820
 821 checkRepTyCon :: (TyCon -> Bool) -> Type -> Bool
 822         -- Look through newtypes
 823         -- Non-recursive ones are transparent to splitTyConApp,
 824         -- but recursive ones aren't; hence the splitNewType_maybe
 825 checkRepTyCon check_tc ty
 826   | Just ty'    <- splitNewType_maybe ty  = checkRepTyCon check_tc ty'
 827   | Just (tc,_) <- splitTyConApp_maybe ty = check_tc tc
 828   | otherwise                             = False
 829 \end{code}
 830
 831 ----------------------------------------------
 832 These chaps do the work; they are not exported
 833 ----------------------------------------------
 834
 835 \begin{code}
 836 legalFEArgTyCon :: TyCon -> Bool
 837 -- It's illegal to return foreign objects and (mutable)
 838 -- bytearrays from a _ccall_ / foreign declaration
 839 -- (or be passed them as arguments in foreign exported functions).
 840 legalFEArgTyCon tc
 841   | getUnique tc `elem` [ foreignObjTyConKey, foreignPtrTyConKey,
 842                           byteArrayTyConKey, mutableByteArrayTyConKey ]
 843   = False
 844   -- It's also illegal to make foreign exports that take unboxed
 845   -- arguments.  The RTS API currently can't invoke such things.  --SDM 7/2000
 846   | otherwise
 847   = boxedMarshalableTyCon tc
 848
 849 legalFIResultTyCon :: DynFlags -> TyCon -> Bool
 850 legalFIResultTyCon dflags tc
 851   | getUnique tc `elem`
 852         [ foreignObjTyConKey, foreignPtrTyConKey,
 853           byteArrayTyConKey, mutableByteArrayTyConKey ]  = False
 854   | tc == unitTyCon = True
 855   | otherwise       = marshalableTyCon dflags tc
 856
 857 legalFEResultTyCon :: TyCon -> Bool
 858 legalFEResultTyCon tc
 859   | getUnique tc `elem`
 860         [ foreignObjTyConKey, foreignPtrTyConKey,
 861           byteArrayTyConKey, mutableByteArrayTyConKey ]  = False
 862   | tc == unitTyCon = True
 863   | otherwise       = boxedMarshalableTyCon tc
 864
 865 legalOutgoingTyCon :: DynFlags -> Safety -> TyCon -> Bool
 866 -- Checks validity of types going from Haskell -> external world
 867 legalOutgoingTyCon dflags safety tc
 868   | playSafe safety && getUnique tc `elem` [byteArrayTyConKey, mutableByteArrayTyConKey]
 869   = False
 870   | otherwise
 871   = marshalableTyCon dflags tc
 872
 873 marshalableTyCon dflags tc
 874   =  (dopt Opt_GlasgowExts dflags && isUnLiftedTyCon tc)
 875   || boxedMarshalableTyCon tc
 876
 877 boxedMarshalableTyCon tc
 878    = getUnique tc `elem` [ intTyConKey, int8TyConKey, int16TyConKey
 879                          , int32TyConKey, int64TyConKey
 880                          , wordTyConKey, word8TyConKey, word16TyConKey
 881                          , word32TyConKey, word64TyConKey
 882                          , floatTyConKey, doubleTyConKey
 883                          , addrTyConKey, ptrTyConKey, funPtrTyConKey
 884                          , charTyConKey, foreignObjTyConKey
 885                          , foreignPtrTyConKey
 886                          , stablePtrTyConKey
 887                          , byteArrayTyConKey, mutableByteArrayTyConKey
 888                          , boolTyConKey
 889                          ]
 890 \end{code}
 891
 892
 893 %************************************************************************
 894 %*                                                                      *
 895 \subsection{Unification with an explicit substitution}
 896 %*                                                                      *
 897 %************************************************************************
 898
 899 (allDistinctTyVars tys tvs) = True
 900         iff
 901 all the types tys are type variables,
 902 distinct from each other and from tvs.
 903
 904 This is useful when checking that unification hasn't unified signature
 905 type variables.  For example, if the type sig is
 906         f :: forall a b. a -> b -> b
 907 we want to check that 'a' and 'b' havn't
 908         (a) been unified with a non-tyvar type
 909         (b) been unified with each other (all distinct)
 910         (c) been unified with a variable free in the environment
 911
 912 \begin{code}
 913 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
 914
 915 allDistinctTyVars []       acc
 916   = True
 917 allDistinctTyVars (ty:tys) acc
 918   = case tcGetTyVar_maybe ty of
 919         Nothing                       -> False  -- (a)
 920         Just tv | tv `elemVarSet` acc -> False  -- (b) or (c)
 921                 | otherwise           -> allDistinctTyVars tys (acc `extendVarSet` tv)
 922 \end{code}
 923
 924
 925 %************************************************************************
 926 %*                                                                      *
 927 \subsection{Unification with an explicit substitution}
 928 %*                                                                      *
 929 %************************************************************************
 930
 931 Unify types with an explicit substitution and no monad.
 932 Ignore usage annotations.
 933
 934 \begin{code}
 935 type MySubst
 936    = (TyVarSet,         -- Set of template tyvars
 937       TyVarSubstEnv)    -- Not necessarily idempotent
 938
 939 unifyTysX :: TyVarSet           -- Template tyvars
 940           -> Type
 941           -> Type
 942           -> Maybe TyVarSubstEnv
 943 unifyTysX tmpl_tyvars ty1 ty2
 944   = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
 945
 946 unifyExtendTysX :: TyVarSet             -- Template tyvars
 947                 -> TyVarSubstEnv        -- Substitution to start with
 948                 -> Type
 949                 -> Type
 950                 -> Maybe TyVarSubstEnv  -- Extended substitution
 951 unifyExtendTysX tmpl_tyvars subst ty1 ty2
 952   = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
 953
 954 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
 955               -> Maybe TyVarSubstEnv
 956 unifyTyListsX tmpl_tyvars tys1 tys2
 957   = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
 958
 959
 960 uTysX :: Type
 961       -> Type
 962       -> (MySubst -> Maybe result)
 963       -> MySubst
 964       -> Maybe result
 965
 966 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
 967 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
 968
 969         -- Variables; go for uVar
 970 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
 971   | tyvar1 == tyvar2
 972   = k subst
 973 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
 974   | tyvar1 `elemVarSet` tmpls
 975   = uVarX tyvar1 ty2 k subst
 976 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
 977   | tyvar2 `elemVarSet` tmpls
 978   = uVarX tyvar2 ty1 k subst
 979
 980         -- Predicates
 981 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
 982   | n1 == n2 = uTysX t1 t2 k subst
 983 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
 984   | c1 == c2 = uTyListsX tys1 tys2 k subst
 985 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
 986   | tc1 == tc2 = uTyListsX tys1 tys2 k subst
 987
 988         -- Functions; just check the two parts
 989 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
 990   = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
 991
 992         -- Type constructors must match
 993 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
 994   | (con1 == con2 && equalLength tys1 tys2)
 995   = uTyListsX tys1 tys2 k subst
 996
 997         -- Applications need a bit of care!
 998         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 999         -- NB: we've already dealt with type variables and Notes,
1000         -- so if one type is an App the other one jolly well better be too
1001 uTysX (AppTy s1 t1) ty2 k subst
1002   = case tcSplitAppTy_maybe ty2 of
1003       Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1004       Nothing       -> Nothing    -- Fail
1005
1006 uTysX ty1 (AppTy s2 t2) k subst
1007   = case tcSplitAppTy_maybe ty1 of
1008       Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
1009       Nothing       -> Nothing    -- Fail
1010
1011         -- Not expecting for-alls in unification
1012 #ifdef DEBUG
1013 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
1014 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
1015 #endif
1016
1017         -- Ignore usages
1018 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
1019 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
1020
1021         -- Anything else fails
1022 uTysX ty1 ty2 k subst = Nothing
1023
1024
1025 uTyListsX []         []         k subst = k subst
1026 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
1027 uTyListsX tys1       tys2       k subst = Nothing   -- Fail if the lists are different lengths
1028 \end{code}
1029
1030 \begin{code}
1031 -- Invariant: tv1 is a unifiable variable
1032 uVarX tv1 ty2 k subst@(tmpls, env)
1033   = case lookupSubstEnv env tv1 of
1034       Just (DoneTy ty1) ->    -- Already bound
1035                      uTysX ty1 ty2 k subst
1036
1037       Nothing        -- Not already bound
1038                |  typeKind ty2 `eqKind` tyVarKind tv1
1039                && occur_check_ok ty2
1040                ->     -- No kind mismatch nor occur check
1041                   UASSERT( not (isUTy ty2) )
1042                   k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
1043
1044                | otherwise -> Nothing   -- Fail if kind mis-match or occur check
1045   where
1046     occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
1047     occur_check_ok_tv tv | tv1 == tv = False
1048                          | otherwise = case lookupSubstEnv env tv of
1049                                          Nothing           -> True
1050                                          Just (DoneTy ty)  -> occur_check_ok ty
1051 \end{code}
1052
1053
1054
1055 %************************************************************************
1056 %*                                                                      *
1057 \subsection{Matching on types}
1058 %*                                                                      *
1059 %************************************************************************
1060
1061 Matching is a {\em unidirectional} process, matching a type against a
1062 template (which is just a type with type variables in it).  The
1063 matcher assumes that there are no repeated type variables in the
1064 template, so that it simply returns a mapping of type variables to
1065 types.  It also fails on nested foralls.
1066
1067 @matchTys@ matches corresponding elements of a list of templates and
1068 types.  It and @matchTy@ both ignore usage annotations, unlike the
1069 main function @match@.
1070
1071 \begin{code}
1072 matchTy :: TyVarSet                     -- Template tyvars
1073         -> Type                         -- Template
1074         -> Type                         -- Proposed instance of template
1075         -> Maybe TyVarSubstEnv          -- Matching substitution
1076
1077
1078 matchTys :: TyVarSet                    -- Template tyvars
1079          -> [Type]                      -- Templates
1080          -> [Type]                      -- Proposed instance of template
1081          -> Maybe (TyVarSubstEnv,               -- Matching substitution
1082                    [Type])              -- Left over instance types
1083
1084 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
1085
1086 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
1087                                       (\ (senv,tys) -> Just (senv,tys))
1088                                       emptySubstEnv
1089 \end{code}
1090
1091 @match@ is the main function.  It takes a flag indicating whether
1092 usage annotations are to be respected.
1093
1094 \begin{code}
1095 match :: Type -> Type                           -- Current match pair
1096       -> TyVarSet                               -- Template vars
1097       -> (TyVarSubstEnv -> Maybe result)        -- Continuation
1098       -> TyVarSubstEnv                          -- Current subst
1099       -> Maybe result
1100
1101 -- When matching against a type variable, see if the variable
1102 -- has already been bound.  If so, check that what it's bound to
1103 -- is the same as ty; if not, bind it and carry on.
1104
1105 match (TyVarTy v) ty tmpls k senv
1106   | v `elemVarSet` tmpls
1107   =     -- v is a template variable
1108     case lookupSubstEnv senv v of
1109         Nothing -> UASSERT( not (isUTy ty) )
1110                    k (extendSubstEnv senv v (DoneTy ty))
1111         Just (DoneTy ty')  | ty' `tcEqType` ty   -> k senv   -- Succeeds
1112                            | otherwise           -> Nothing  -- Fails
1113
1114   | otherwise
1115   =     -- v is not a template variable; ty had better match
1116         -- Can't use (==) because types differ
1117     case tcGetTyVar_maybe ty of
1118         Just v' | v == v' -> k senv    -- Success
1119         other             -> Nothing   -- Failure
1120     -- This tcGetTyVar_maybe is *required* because it must strip Notes.
1121     -- I guess the reason the Note-stripping case is *last* rather than first
1122     -- is to preserve type synonyms etc., so I'm not moving it to the
1123     -- top; but this means that (without the deNotetype) a type
1124     -- variable may not match the pattern (TyVarTy v') as one would
1125     -- expect, due to an intervening Note.  KSW 2000-06.
1126
1127         -- Predicates
1128 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
1129   | n1 == n2 = match t1 t2 tmpls k senv
1130 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
1131   | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
1132 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1133   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1134
1135         -- Functions; just check the two parts
1136 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
1137   = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
1138
1139 match (AppTy fun1 arg1) ty2 tmpls k senv
1140   = case tcSplitAppTy_maybe ty2 of
1141         Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
1142         Nothing          -> Nothing     -- Fail
1143
1144 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
1145   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1146
1147 -- Newtypes are opaque; other source types should not happen
1148 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
1149   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
1150
1151 match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
1152 match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1153
1154         -- With type synonyms, we have to be careful for the exact
1155         -- same reasons as in the unifier.  Please see the
1156         -- considerable commentary there before changing anything
1157         -- here! (WDP 95/05)
1158 match (NoteTy n1 ty1) ty2      tmpls k senv = match ty1 ty2 tmpls k senv
1159 match ty1      (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
1160
1161 -- Catch-all fails
1162 match _ _ _ _ _ = Nothing
1163
1164 match_list_exactly tys1 tys2 tmpls k senv
1165   = match_list tys1 tys2 tmpls k' senv
1166   where
1167     k' (senv', tys2') | null tys2' = k senv'    -- Succeed
1168                       | otherwise  = Nothing    -- Fail
1169
1170 match_list []         tys2       tmpls k senv = k (senv, tys2)
1171 match_list (ty1:tys1) []         tmpls k senv = Nothing -- Not enough arg tys => failure
1172 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
1173   = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv
1174 \end{code}