ghc/compiler/typecheck/TcType.lhs

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