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