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