ghc/compiler/typecheck/TcType.lhs

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