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