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