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