ghc/compiler/typecheck/TcType.lhs

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