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