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