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