ghc/compiler/typecheck/TcType.lhs

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