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