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