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