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