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