ghc/compiler/typecheck/TcType.lhs

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