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