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   TauType, RhoType, SigmaType,
  21
  22   --------------------------------
  23   -- Builders
  24   mkRhoTy, mkSigmaTy,
  25
  26   --------------------------------
  27   -- Splitters
  28   -- These are important because they do not look through newtypes
  29   tcSplitForAllTys, tcSplitRhoTy,
  30   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy,
  31   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
  32   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitSigmaTy,
  33   tcSplitMethodTy, tcGetTyVar_maybe, tcGetTyVar,
  34
  35   ---------------------------------
  36   -- Predicates.
  37   -- Again, newtypes are opaque
  38   tcEqType, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred,
  39   isQualifiedTy, isOverloadedTy, isStrictType, isStrictPred,
  40   isDoubleTy, isFloatTy, isIntTy,
  41   isIntegerTy, isAddrTy, isBoolTy, isUnitTy, isForeignPtrTy, isPrimitiveType,
  42   isTauTy, tcIsTyVarTy, tcIsForAllTy,
  43
  44   ---------------------------------
  45   -- Misc type manipulators
  46   hoistForAllTys, deNoteType,
  47   namesOfType, namesOfDFunHead,
  48   getDFunTyKey,
  49
  50   ---------------------------------
  51   -- Predicate types
  52   PredType, mkPredTy, mkPredTys, getClassPredTys_maybe, getClassPredTys,
  53   isPredTy, isClassPred, isTyVarClassPred, predHasFDs,
  54   mkDictTy, tcSplitPredTy_maybe, predTyUnique,
  55   isDictTy, tcSplitDFunTy, predTyUnique,
  56   mkClassPred, predMentionsIPs, inheritablePred, isIPPred, mkPredName,
  57
  58   ---------------------------------
  59   -- Unifier and matcher
  60   unifyTysX, unifyTyListsX, unifyExtendTysX,
  61   allDistinctTyVars,
  62   matchTy, matchTys, match,
  63
  64   --------------------------------
  65   -- Rexported from Type
  66   Kind,         -- Stuff to do with kinds is insensitive to pre/post Tc
  67   unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
  68   superBoxity, liftedBoxity, hasMoreBoxityInfo, defaultKind, superKind,
  69   isTypeKind,
  70
  71   Type, SourceType(..), PredType, ThetaType,
  72   mkForAllTy, mkForAllTys,
  73   mkFunTy, mkFunTys, zipFunTys,
  74   mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
  75   mkTyVarTy, mkTyVarTys, mkTyConTy,
  76
  77   isUnLiftedType,       -- Source types are always lifted
  78   isUnboxedTupleType,   -- Ditto
  79
  80   tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
  81   tidyTyVar, tidyTyVars,
  82   typeKind, eqKind, eqUsage,
  83
  84   tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta
  85   ) where
  86
  87 #include "HsVersions.h"
  88
  89
  90 import {-# SOURCE #-} PprType( pprType )
  91
  92 -- friends:
  93 import TypeRep          ( Type(..), TyNote(..), funTyCon )  -- friend
  94 import Type             ( mkUTyM, unUTy )       -- Used locally
  95
  96 import Type             (       -- Re-exports
  97                           tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, tyVarsOfTheta,
  98                           Kind, Type, TauType, SourceType(..), PredType, ThetaType,
  99                           unliftedTypeKind, liftedTypeKind, openTypeKind, mkArrowKind, mkArrowKinds,
 100                           mkForAllTy, mkForAllTys, defaultKind, isTypeKind,
 101                           mkFunTy, mkFunTys, zipFunTys,
 102                           mkTyConApp, mkAppTy, mkAppTys, mkSynTy, applyTy, applyTys,
 103                           mkTyVarTy, mkTyVarTys, mkTyConTy,
 104                           isUnLiftedType, isUnboxedTupleType,
 105                           tidyTopType, tidyType, tidyPred, tidyTypes, tidyFreeTyVars, tidyOpenType, tidyOpenTypes,
 106                           tidyTyVar, tidyTyVars, eqKind, eqUsage,
 107                           hasMoreBoxityInfo, liftedBoxity, superBoxity, typeKind, superKind
 108                         )
 109 import TyCon            ( TyCon, isPrimTyCon, tyConArity, isNewTyCon )
 110 import Class            ( classTyCon, classHasFDs, Class )
 111 import Var              ( TyVar, tyVarKind )
 112 import VarEnv
 113 import VarSet
 114
 115 -- others:
 116 import CmdLineOpts      ( opt_DictsStrict )
 117 import Name             ( Name, NamedThing(..), mkLocalName )
 118 import OccName          ( OccName, mkDictOcc )
 119 import NameSet
 120 import PrelNames        ( floatTyConKey, doubleTyConKey, foreignPtrTyConKey,
 121                           integerTyConKey, intTyConKey, addrTyConKey, boolTyConKey )
 122 import Unique           ( Unique, Uniquable(..), mkTupleTyConUnique )
 123 import SrcLoc           ( SrcLoc )
 124 import Util             ( cmpList, thenCmp )
 125 import Maybes           ( maybeToBool, expectJust )
 126 import BasicTypes       ( Boxity(..) )
 127 import Outputable
 128 \end{code}
 129
 130
 131 %************************************************************************
 132 %*                                                                      *
 133 \subsection{Tau, sigma and rho}
 134 %*                                                                      *
 135 %************************************************************************
 136
 137 \begin{code}
 138 type SigmaType    = Type
 139 type RhoType      = Type
 140
 141 mkSigmaTy tyvars theta tau = mkForAllTys tyvars (mkRhoTy theta tau)
 142
 143 mkRhoTy :: [SourceType] -> Type -> Type
 144 mkRhoTy theta ty = UASSERT2( not (isUTy ty), pprType ty )
 145                    foldr (\p r -> FunTy (mkUTyM (mkPredTy p)) (mkUTyM r)) ty theta
 146
 147 \end{code}
 148
 149
 150 @isTauTy@ tests for nested for-alls.
 151
 152 \begin{code}
 153 isTauTy :: Type -> Bool
 154 isTauTy (TyVarTy v)      = True
 155 isTauTy (TyConApp _ tys) = all isTauTy tys
 156 isTauTy (AppTy a b)      = isTauTy a && isTauTy b
 157 isTauTy (FunTy a b)      = isTauTy a && isTauTy b
 158 isTauTy (SourceTy p)     = True         -- Don't look through source types
 159 isTauTy (NoteTy _ ty)    = isTauTy ty
 160 isTauTy (UsageTy _ ty)   = isTauTy ty
 161 isTauTy other            = False
 162 \end{code}
 163
 164 \begin{code}
 165 getDFunTyKey :: Type -> OccName -- Get some string from a type, to be used to
 166                                 -- construct a dictionary function name
 167 getDFunTyKey (TyVarTy tv)            = getOccName tv
 168 getDFunTyKey (TyConApp tc _)         = getOccName tc
 169 getDFunTyKey (AppTy fun _)           = getDFunTyKey fun
 170 getDFunTyKey (NoteTy _ t)            = getDFunTyKey t
 171 getDFunTyKey (FunTy arg _)           = getOccName funTyCon
 172 getDFunTyKey (ForAllTy _ t)          = getDFunTyKey t
 173 getDFunTyKey (UsageTy _ t)           = getDFunTyKey t
 174 getDFunTyKey (SourceTy (NType tc _)) = getOccName tc    -- Newtypes are quite reasonable
 175 getDFunTyKey ty                      = pprPanic "getDFunTyKey" (pprType ty)
 176 -- SourceTy shouldn't happen
 177 \end{code}
 178
 179
 180 %************************************************************************
 181 %*                                                                      *
 182 \subsection{Expanding and splitting}
 183 %*                                                                      *
 184 %************************************************************************
 185
 186 These tcSplit functions are like their non-Tc analogues, but
 187         a) they do not look through newtypes
 188         b) they do not look through PredTys
 189         c) [future] they ignore usage-type annotations
 190
 191 However, they are non-monadic and do not follow through mutable type
 192 variables.  It's up to you to make sure this doesn't matter.
 193
 194 \begin{code}
 195 tcSplitForAllTys :: Type -> ([TyVar], Type)
 196 tcSplitForAllTys ty = split ty ty []
 197    where
 198      split orig_ty (ForAllTy tv ty) tvs = split ty ty (tv:tvs)
 199      split orig_ty (NoteTy n  ty)   tvs = split orig_ty ty tvs
 200      split orig_ty (UsageTy _ ty)   tvs = split orig_ty ty tvs
 201      split orig_ty t                tvs = (reverse tvs, orig_ty)
 202
 203 tcIsForAllTy (ForAllTy tv ty) = True
 204 tcIsForAllTy (NoteTy n ty)    = tcIsForAllTy ty
 205 tcIsForAllTy (UsageTy n ty)   = tcIsForAllTy ty
 206 tcIsForAllTy t                = False
 207
 208 tcSplitRhoTy :: Type -> ([PredType], Type)
 209 tcSplitRhoTy ty = split ty ty []
 210  where
 211   split orig_ty (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
 212                                         Just p  -> split res res (p:ts)
 213                                         Nothing -> (reverse ts, orig_ty)
 214   split orig_ty (NoteTy n ty)   ts = split orig_ty ty ts
 215   split orig_ty (UsageTy _ ty)  ts = split orig_ty ty ts
 216   split orig_ty ty              ts = (reverse ts, orig_ty)
 217
 218 tcSplitSigmaTy ty = case tcSplitForAllTys ty of
 219                         (tvs, rho) -> case tcSplitRhoTy rho of
 220                                         (theta, tau) -> (tvs, theta, tau)
 221
 222 tcTyConAppTyCon :: Type -> TyCon
 223 tcTyConAppTyCon ty = fst (tcSplitTyConApp ty)
 224
 225 tcTyConAppArgs :: Type -> [Type]
 226 tcTyConAppArgs ty = snd (tcSplitTyConApp ty)
 227
 228 tcSplitTyConApp :: Type -> (TyCon, [Type])
 229 tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
 230                         Just stuff -> stuff
 231                         Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 232
 233 tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
 234 -- Newtypes are opaque, so they may be split
 235 tcSplitTyConApp_maybe (TyConApp tc tys)         = Just (tc, tys)
 236 tcSplitTyConApp_maybe (FunTy arg res)           = Just (funTyCon, [unUTy arg,unUTy res])
 237 tcSplitTyConApp_maybe (NoteTy n ty)             = tcSplitTyConApp_maybe ty
 238 tcSplitTyConApp_maybe (UsageTy _ ty)            = tcSplitTyConApp_maybe ty
 239 tcSplitTyConApp_maybe (SourceTy (NType tc tys)) = Just (tc,tys)
 240         -- However, predicates are not treated
 241         -- as tycon applications by the type checker
 242 tcSplitTyConApp_maybe other                     = Nothing
 243
 244 tcSplitFunTys :: Type -> ([Type], Type)
 245 tcSplitFunTys ty = case tcSplitFunTy_maybe ty of
 246                         Nothing        -> ([], ty)
 247                         Just (arg,res) -> (arg:args, res')
 248                                        where
 249                                           (args,res') = tcSplitFunTys res
 250
 251 tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
 252 tcSplitFunTy_maybe (FunTy arg res)  = Just (arg, res)
 253 tcSplitFunTy_maybe (NoteTy n ty)    = tcSplitFunTy_maybe ty
 254 tcSplitFunTy_maybe (UsageTy _ ty)   = tcSplitFunTy_maybe ty
 255 tcSplitFunTy_maybe other            = Nothing
 256
 257 tcFunArgTy    ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> arg }
 258 tcFunResultTy ty = case tcSplitFunTy_maybe ty of { Just (arg,res) -> res }
 259
 260
 261 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
 262 tcSplitAppTy_maybe (FunTy ty1 ty2)           = Just (TyConApp funTyCon [unUTy ty1], unUTy ty2)
 263 tcSplitAppTy_maybe (AppTy ty1 ty2)           = Just (ty1, ty2)
 264 tcSplitAppTy_maybe (NoteTy n ty)             = tcSplitAppTy_maybe ty
 265 tcSplitAppTy_maybe (UsageTy _ ty)            = tcSplitAppTy_maybe ty
 266 tcSplitAppTy_maybe (SourceTy (NType tc tys)) = tc_split_app tc tys
 267         --- Don't forget that newtype!
 268 tcSplitAppTy_maybe (TyConApp tc tys)         = tc_split_app tc tys
 269 tcSplitAppTy_maybe other                     = Nothing
 270
 271 tc_split_app tc []  = Nothing
 272 tc_split_app tc tys = split tys []
 273                     where
 274                       split [ty2]    acc = Just (TyConApp tc (reverse acc), ty2)
 275                       split (ty:tys) acc = split tys (ty:acc)
 276
 277 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
 278                     Just stuff -> stuff
 279                     Nothing    -> pprPanic "tcSplitAppTy" (pprType ty)
 280
 281 tcGetTyVar_maybe :: Type -> Maybe TyVar
 282 tcGetTyVar_maybe (TyVarTy tv)   = Just tv
 283 tcGetTyVar_maybe (NoteTy _ t)   = tcGetTyVar_maybe t
 284 tcGetTyVar_maybe ty@(UsageTy _ _) = pprPanic "tcGetTyVar_maybe: UTy:" (pprType ty)
 285 tcGetTyVar_maybe other          = Nothing
 286
 287 tcGetTyVar :: String -> Type -> TyVar
 288 tcGetTyVar msg ty = expectJust msg (tcGetTyVar_maybe ty)
 289
 290 tcIsTyVarTy :: Type -> Bool
 291 tcIsTyVarTy ty = maybeToBool (tcGetTyVar_maybe ty)
 292 \end{code}
 293
 294 The type of a method for class C is always of the form:
 295         Forall a1..an. C a1..an => sig_ty
 296 where sig_ty is the type given by the method's signature, and thus in general
 297 is a ForallTy.  At the point that splitMethodTy is called, it is expected
 298 that the outer Forall has already been stripped off.  splitMethodTy then
 299 returns (C a1..an, sig_ty') where sig_ty' is sig_ty with any Notes or
 300 Usages stripped off.
 301
 302 \begin{code}
 303 tcSplitMethodTy :: Type -> (PredType, Type)
 304 tcSplitMethodTy ty = split ty
 305  where
 306   split (FunTy arg res) = case tcSplitPredTy_maybe arg of
 307                             Just p  -> (p, res)
 308                             Nothing -> panic "splitMethodTy"
 309   split (NoteTy n ty)   = split ty
 310   split (UsageTy _ ty)  = split ty
 311   split _               = panic "splitMethodTy"
 312
 313 tcSplitDFunTy :: Type -> ([TyVar], [SourceType], Class, [Type])
 314 -- Split the type of a dictionary function
 315 tcSplitDFunTy ty
 316   = case tcSplitSigmaTy ty       of { (tvs, theta, tau) ->
 317     case tcSplitPredTy_maybe tau of { Just (ClassP clas tys) ->
 318     (tvs, theta, clas, tys) }}
 319 \end{code}
 320
 321
 322 %************************************************************************
 323 %*                                                                      *
 324 \subsection{Predicate types}
 325 %*                                                                      *
 326 %************************************************************************
 327
 328 "Predicates" are particular source types, namelyClassP or IParams
 329
 330 \begin{code}
 331 isPred :: SourceType -> Bool
 332 isPred (ClassP _ _) = True
 333 isPred (IParam _ _) = True
 334 isPred (NType _ __) = False
 335
 336 isPredTy :: Type -> Bool
 337 isPredTy (NoteTy _ ty)  = isPredTy ty
 338 isPredTy (UsageTy _ ty) = isPredTy ty
 339 isPredTy (SourceTy sty) = isPred sty
 340 isPredTy _              = False
 341
 342 tcSplitPredTy_maybe :: Type -> Maybe PredType
 343    -- Returns Just for predicates only
 344 tcSplitPredTy_maybe (NoteTy _ ty)           = tcSplitPredTy_maybe ty
 345 tcSplitPredTy_maybe (UsageTy _ ty)          = tcSplitPredTy_maybe ty
 346 tcSplitPredTy_maybe (SourceTy p) | isPred p = Just p
 347 tcSplitPredTy_maybe other                   = Nothing
 348
 349 mkPredTy :: PredType -> Type
 350 mkPredTy pred = SourceTy pred
 351
 352 mkPredTys :: ThetaType -> [Type]
 353 mkPredTys preds = map SourceTy preds
 354
 355 predTyUnique :: PredType -> Unique
 356 predTyUnique (IParam n _)      = getUnique n
 357 predTyUnique (ClassP clas tys) = getUnique clas
 358
 359 predHasFDs :: PredType -> Bool
 360 -- True if the predicate has functional depenencies;
 361 -- I.e. should participate in improvement
 362 predHasFDs (IParam _ _)   = True
 363 predHasFDs (ClassP cls _) = classHasFDs cls
 364
 365 mkPredName :: Unique -> SrcLoc -> SourceType -> Name
 366 mkPredName uniq loc (ClassP cls tys) = mkLocalName uniq (mkDictOcc (getOccName cls)) loc
 367 mkPredName uniq loc (IParam name ty) = name
 368 \end{code}
 369
 370
 371 --------------------- Dictionary types ---------------------------------
 372
 373 \begin{code}
 374 mkClassPred clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
 375                        ClassP clas tys
 376
 377 isClassPred :: SourceType -> Bool
 378 isClassPred (ClassP clas tys) = True
 379 isClassPred other             = False
 380
 381 isTyVarClassPred (ClassP clas tys) = all tcIsTyVarTy tys
 382 isTyVarClassPred other             = False
 383
 384 getClassPredTys_maybe :: SourceType -> Maybe (Class, [Type])
 385 getClassPredTys_maybe (ClassP clas tys) = Just (clas, tys)
 386 getClassPredTys_maybe _                 = Nothing
 387
 388 getClassPredTys :: PredType -> (Class, [Type])
 389 getClassPredTys (ClassP clas tys) = (clas, tys)
 390
 391 mkDictTy :: Class -> [Type] -> Type
 392 mkDictTy clas tys = UASSERT2( not (any isUTy tys), ppr clas <+> fsep (map pprType tys) )
 393                     mkPredTy (ClassP clas tys)
 394
 395 isDictTy :: Type -> Bool
 396 isDictTy (SourceTy p)   = isClassPred p
 397 isDictTy (NoteTy _ ty)  = isDictTy ty
 398 isDictTy (UsageTy _ ty) = isDictTy ty
 399 isDictTy other          = False
 400 \end{code}
 401
 402 --------------------- Implicit parameters ---------------------------------
 403
 404 \begin{code}
 405 isIPPred :: SourceType -> Bool
 406 isIPPred (IParam _ _) = True
 407 isIPPred other        = False
 408
 409 inheritablePred :: PredType -> Bool
 410 -- Can be inherited by a context.  For example, consider
 411 --      f x = let g y = (?v, y+x)
 412 --            in (g 3 with ?v = 8,
 413 --                g 4 with ?v = 9)
 414 -- The point is that g's type must be quantifed over ?v:
 415 --      g :: (?v :: a) => a -> a
 416 -- but it doesn't need to be quantified over the Num a dictionary
 417 -- which can be free in g's rhs, and shared by both calls to g
 418 inheritablePred (ClassP _ _) = True
 419 inheritablePred other        = False
 420
 421 predMentionsIPs :: SourceType -> NameSet -> Bool
 422 predMentionsIPs (IParam n _) ns = n `elemNameSet` ns
 423 predMentionsIPs other        ns = False
 424 \end{code}
 425
 426
 427 %************************************************************************
 428 %*                                                                      *
 429 \subsection{Comparison}
 430 %*                                                                      *
 431 %************************************************************************
 432
 433 Comparison, taking note of newtypes, predicates, etc,
 434 But ignoring usage types
 435
 436 \begin{code}
 437 tcEqType :: Type -> Type -> Bool
 438 tcEqType ty1 ty2 = case ty1 `tcCmpType` ty2 of { EQ -> True; other -> False }
 439
 440 tcEqPred :: PredType -> PredType -> Bool
 441 tcEqPred p1 p2 = case p1 `tcCmpPred` p2 of { EQ -> True; other -> False }
 442
 443 -------------
 444 tcCmpType :: Type -> Type -> Ordering
 445 tcCmpType ty1 ty2 = cmpTy emptyVarEnv ty1 ty2
 446
 447 tcCmpTypes tys1 tys2 = cmpTys emptyVarEnv tys1 tys2
 448
 449 tcCmpPred p1 p2 = cmpSourceTy emptyVarEnv p1 p2
 450 -------------
 451 cmpTys env tys1 tys2 = cmpList (cmpTy env) tys1 tys2
 452
 453 -------------
 454 cmpTy :: TyVarEnv TyVar -> Type -> Type -> Ordering
 455   -- The "env" maps type variables in ty1 to type variables in ty2
 456   -- So when comparing for-alls.. (forall tv1 . t1) (forall tv2 . t2)
 457   -- we in effect substitute tv2 for tv1 in t1 before continuing
 458
 459     -- Look through NoteTy and UsageTy
 460 cmpTy env (NoteTy _ ty1) ty2 = cmpTy env ty1 ty2
 461 cmpTy env ty1 (NoteTy _ ty2) = cmpTy env ty1 ty2
 462 cmpTy env (UsageTy _ ty1) ty2 = cmpTy env ty1 ty2
 463 cmpTy env ty1 (UsageTy _ ty2) = cmpTy env ty1 ty2
 464
 465     -- Deal with equal constructors
 466 cmpTy env (TyVarTy tv1) (TyVarTy tv2) = case lookupVarEnv env tv1 of
 467                                           Just tv1a -> tv1a `compare` tv2
 468                                           Nothing   -> tv1  `compare` tv2
 469
 470 cmpTy env (SourceTy p1) (SourceTy p2) = cmpSourceTy env p1 p2
 471 cmpTy env (AppTy f1 a1) (AppTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
 472 cmpTy env (FunTy f1 a1) (FunTy f2 a2) = cmpTy env f1 f2 `thenCmp` cmpTy env a1 a2
 473 cmpTy env (TyConApp tc1 tys1) (TyConApp tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
 474 cmpTy env (ForAllTy tv1 t1)   (ForAllTy tv2 t2)   = cmpTy (extendVarEnv env tv1 tv2) t1 t2
 475
 476     -- Deal with the rest: TyVarTy < AppTy < FunTy < TyConApp < ForAllTy < SourceTy
 477 cmpTy env (AppTy _ _) (TyVarTy _) = GT
 478
 479 cmpTy env (FunTy _ _) (TyVarTy _) = GT
 480 cmpTy env (FunTy _ _) (AppTy _ _) = GT
 481
 482 cmpTy env (TyConApp _ _) (TyVarTy _) = GT
 483 cmpTy env (TyConApp _ _) (AppTy _ _) = GT
 484 cmpTy env (TyConApp _ _) (FunTy _ _) = GT
 485
 486 cmpTy env (ForAllTy _ _) (TyVarTy _)    = GT
 487 cmpTy env (ForAllTy _ _) (AppTy _ _)    = GT
 488 cmpTy env (ForAllTy _ _) (FunTy _ _)    = GT
 489 cmpTy env (ForAllTy _ _) (TyConApp _ _) = GT
 490
 491 cmpTy env (SourceTy _)   t2             = GT
 492
 493 cmpTy env _ _ = LT
 494 \end{code}
 495
 496 \begin{code}
 497 cmpSourceTy :: TyVarEnv TyVar -> SourceType -> SourceType -> Ordering
 498 cmpSourceTy env (IParam n1 ty1)   (IParam n2 ty2) = (n1 `compare` n2) `thenCmp` (cmpTy env ty1 ty2)
 499         -- Compare types as well as names for implicit parameters
 500         -- This comparison is used exclusively (I think) for the
 501         -- finite map built in TcSimplify
 502 cmpSourceTy env (IParam _ _)     sty              = LT
 503
 504 cmpSourceTy env (ClassP _ _)     (IParam _ _)     = GT
 505 cmpSourceTy env (ClassP c1 tys1) (ClassP c2 tys2) = (c1 `compare` c2) `thenCmp` (cmpTys env tys1 tys2)
 506 cmpSourceTy env (ClassP _ _)     (NType _ _)      = LT
 507
 508 cmpSourceTy env (NType tc1 tys1) (NType tc2 tys2) = (tc1 `compare` tc2) `thenCmp` (cmpTys env tys1 tys2)
 509 cmpSourceTy env (NType _ _)      sty              = GT
 510 \end{code}
 511
 512 PredTypes are used as a FM key in TcSimplify,
 513 so we take the easy path and make them an instance of Ord
 514
 515 \begin{code}
 516 instance Eq  SourceType where { (==)    = tcEqPred }
 517 instance Ord SourceType where { compare = tcCmpPred }
 518 \end{code}
 519
 520
 521 %************************************************************************
 522 %*                                                                      *
 523 \subsection{Predicates}
 524 %*                                                                      *
 525 %************************************************************************
 526
 527 isQualifiedTy returns true of any qualified type.  It doesn't *necessarily* have
 528 any foralls.  E.g.
 529         f :: (?x::Int) => Int -> Int
 530
 531 \begin{code}
 532 isQualifiedTy :: Type -> Bool
 533 isQualifiedTy (ForAllTy tyvar ty) = True
 534 isQualifiedTy (FunTy a b)         = isPredTy a
 535 isQualifiedTy (NoteTy n ty)       = isQualifiedTy ty
 536 isQualifiedTy (UsageTy _ ty)      = isQualifiedTy ty
 537 isQualifiedTy _                   = False
 538
 539 isOverloadedTy :: Type -> Bool
 540 isOverloadedTy (ForAllTy tyvar ty) = isOverloadedTy ty
 541 isOverloadedTy (FunTy a b)         = isPredTy a
 542 isOverloadedTy (NoteTy n ty)       = isOverloadedTy ty
 543 isOverloadedTy (UsageTy _ ty)      = isOverloadedTy ty
 544 isOverloadedTy _                   = False
 545 \end{code}
 546
 547 \begin{code}
 548 isFloatTy      = is_tc floatTyConKey
 549 isDoubleTy     = is_tc doubleTyConKey
 550 isForeignPtrTy = is_tc foreignPtrTyConKey
 551 isIntegerTy    = is_tc integerTyConKey
 552 isIntTy        = is_tc intTyConKey
 553 isAddrTy       = is_tc addrTyConKey
 554 isBoolTy       = is_tc boolTyConKey
 555 isUnitTy       = is_tc (mkTupleTyConUnique Boxed 0)
 556
 557 is_tc :: Unique -> Type -> Bool
 558 -- Newtypes are opaque to this
 559 is_tc uniq ty = case tcSplitTyConApp_maybe ty of
 560                         Just (tc, _) -> uniq == getUnique tc
 561                         Nothing      -> False
 562 \end{code}
 563
 564 \begin{code}
 565 isPrimitiveType :: Type -> Bool
 566 -- Returns types that are opaque to Haskell.
 567 -- Most of these are unlifted, but now that we interact with .NET, we
 568 -- may have primtive (foreign-imported) types that are lifted
 569 isPrimitiveType ty = case tcSplitTyConApp_maybe ty of
 570                         Just (tc, ty_args) -> ASSERT( length ty_args == tyConArity tc )
 571                                               isPrimTyCon tc
 572                         other              -> False
 573 \end{code}
 574
 575 @isStrictType@ computes whether an argument (or let RHS) should
 576 be computed strictly or lazily, based only on its type
 577
 578 \begin{code}
 579 isStrictType :: Type -> Bool
 580 isStrictType ty
 581   | isUnLiftedType ty                   = True
 582   | Just pred <- tcSplitPredTy_maybe ty = isStrictPred pred
 583   | otherwise                           = False
 584
 585 isStrictPred (ClassP clas _) =  opt_DictsStrict
 586                              && not (isNewTyCon (classTyCon clas))
 587 isStrictPred pred            =  False
 588         -- We may be strict in dictionary types, but only if it
 589         -- has more than one component.
 590         -- [Being strict in a single-component dictionary risks
 591         --  poking the dictionary component, which is wrong.]
 592 \end{code}
 593
 594
 595 %************************************************************************
 596 %*                                                                      *
 597 \subsection{Misc}
 598 %*                                                                      *
 599 %************************************************************************
 600
 601 \begin{code}
 602 hoistForAllTys :: Type -> Type
 603         -- Move all the foralls to the top
 604         -- e.g.  T -> forall a. a  ==>   forall a. T -> a
 605         -- Careful: LOSES USAGE ANNOTATIONS!
 606 hoistForAllTys ty
 607   = case hoist ty of { (tvs, body) -> mkForAllTys tvs body }
 608   where
 609     hoist :: Type -> ([TyVar], Type)
 610     hoist ty = case tcSplitFunTys    ty  of { (args, res) ->
 611                case tcSplitForAllTys res of {
 612                   ([], body)  -> ([], ty) ;
 613                   (tvs1, body1) -> case hoist body1 of { (tvs2,body2) ->
 614                                    (tvs1 ++ tvs2, mkFunTys args body2)
 615                }}}
 616 \end{code}
 617
 618
 619 \begin{code}
 620 deNoteType :: Type -> Type
 621         -- Remove synonyms, but not source types
 622 deNoteType ty@(TyVarTy tyvar)   = ty
 623 deNoteType (TyConApp tycon tys) = TyConApp tycon (map deNoteType tys)
 624 deNoteType (SourceTy p)         = SourceTy (deNoteSourceType p)
 625 deNoteType (NoteTy _ ty)        = deNoteType ty
 626 deNoteType (AppTy fun arg)      = AppTy (deNoteType fun) (deNoteType arg)
 627 deNoteType (FunTy fun arg)      = FunTy (deNoteType fun) (deNoteType arg)
 628 deNoteType (ForAllTy tv ty)     = ForAllTy tv (deNoteType ty)
 629 deNoteType (UsageTy u ty)       = UsageTy u (deNoteType ty)
 630
 631 deNoteSourceType :: SourceType -> SourceType
 632 deNoteSourceType (ClassP c tys) = ClassP c (map deNoteType tys)
 633 deNoteSourceType (IParam n ty)  = IParam n (deNoteType ty)
 634 deNoteSourceType (NType tc tys) = NType tc (map deNoteType tys)
 635 \end{code}
 636
 637 Find the free names of a type, including the type constructors and classes it mentions
 638 This is used in the front end of the compiler
 639
 640 \begin{code}
 641 namesOfType :: Type -> NameSet
 642 namesOfType (TyVarTy tv)                = unitNameSet (getName tv)
 643 namesOfType (TyConApp tycon tys)        = unitNameSet (getName tycon) `unionNameSets` namesOfTypes tys
 644 namesOfType (NoteTy (SynNote ty1) ty2)  = namesOfType ty1
 645 namesOfType (NoteTy other_note    ty2)  = namesOfType ty2
 646 namesOfType (SourceTy (IParam n ty))    = namesOfType ty
 647 namesOfType (SourceTy (ClassP cl tys))  = unitNameSet (getName cl) `unionNameSets` namesOfTypes tys
 648 namesOfType (SourceTy (NType tc tys))   = unitNameSet (getName tc) `unionNameSets` namesOfTypes tys
 649 namesOfType (FunTy arg res)             = namesOfType arg `unionNameSets` namesOfType res
 650 namesOfType (AppTy fun arg)             = namesOfType fun `unionNameSets` namesOfType arg
 651 namesOfType (ForAllTy tyvar ty)         = namesOfType ty `delFromNameSet` getName tyvar
 652 namesOfType (UsageTy u ty)              = namesOfType u `unionNameSets` namesOfType ty
 653
 654 namesOfTypes tys = foldr (unionNameSets . namesOfType) emptyNameSet tys
 655
 656 namesOfDFunHead :: Type -> NameSet
 657 -- Find the free type constructors and classes
 658 -- of the head of the dfun instance type
 659 -- The 'dfun_head_type' is because of
 660 --      instance Foo a => Baz T where ...
 661 -- The decl is an orphan if Baz and T are both not locally defined,
 662 --      even if Foo *is* locally defined
 663 namesOfDFunHead dfun_ty = case tcSplitSigmaTy dfun_ty of
 664                                 (tvs,_,head_ty) -> delListFromNameSet (namesOfType head_ty)
 665                                                                       (map getName tvs)
 666 \end{code}
 667
 668
 669 %************************************************************************
 670 %*                                                                      *
 671 \subsection{Unification with an explicit substitution}
 672 %*                                                                      *
 673 %************************************************************************
 674
 675 (allDistinctTyVars tys tvs) = True
 676         iff
 677 all the types tys are type variables,
 678 distinct from each other and from tvs.
 679
 680 This is useful when checking that unification hasn't unified signature
 681 type variables.  For example, if the type sig is
 682         f :: forall a b. a -> b -> b
 683 we want to check that 'a' and 'b' havn't
 684         (a) been unified with a non-tyvar type
 685         (b) been unified with each other (all distinct)
 686         (c) been unified with a variable free in the environment
 687
 688 \begin{code}
 689 allDistinctTyVars :: [Type] -> TyVarSet -> Bool
 690
 691 allDistinctTyVars []       acc
 692   = True
 693 allDistinctTyVars (ty:tys) acc
 694   = case tcGetTyVar_maybe ty of
 695         Nothing                       -> False  -- (a)
 696         Just tv | tv `elemVarSet` acc -> False  -- (b) or (c)
 697                 | otherwise           -> allDistinctTyVars tys (acc `extendVarSet` tv)
 698 \end{code}
 699
 700
 701 %************************************************************************
 702 %*                                                                      *
 703 \subsection{Unification with an explicit substitution}
 704 %*                                                                      *
 705 %************************************************************************
 706
 707 Unify types with an explicit substitution and no monad.
 708 Ignore usage annotations.
 709
 710 \begin{code}
 711 type MySubst
 712    = (TyVarSet,         -- Set of template tyvars
 713       TyVarSubstEnv)    -- Not necessarily idempotent
 714
 715 unifyTysX :: TyVarSet           -- Template tyvars
 716           -> Type
 717           -> Type
 718           -> Maybe TyVarSubstEnv
 719 unifyTysX tmpl_tyvars ty1 ty2
 720   = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
 721
 722 unifyExtendTysX :: TyVarSet             -- Template tyvars
 723                 -> TyVarSubstEnv        -- Substitution to start with
 724                 -> Type
 725                 -> Type
 726                 -> Maybe TyVarSubstEnv  -- Extended substitution
 727 unifyExtendTysX tmpl_tyvars subst ty1 ty2
 728   = uTysX ty1 ty2 (\(_,s) -> Just s) (tmpl_tyvars, subst)
 729
 730 unifyTyListsX :: TyVarSet -> [Type] -> [Type]
 731               -> Maybe TyVarSubstEnv
 732 unifyTyListsX tmpl_tyvars tys1 tys2
 733   = uTyListsX tys1 tys2 (\(_,s) -> Just s) (tmpl_tyvars, emptySubstEnv)
 734
 735
 736 uTysX :: Type
 737       -> Type
 738       -> (MySubst -> Maybe result)
 739       -> MySubst
 740       -> Maybe result
 741
 742 uTysX (NoteTy _ ty1) ty2 k subst = uTysX ty1 ty2 k subst
 743 uTysX ty1 (NoteTy _ ty2) k subst = uTysX ty1 ty2 k subst
 744
 745         -- Variables; go for uVar
 746 uTysX (TyVarTy tyvar1) (TyVarTy tyvar2) k subst
 747   | tyvar1 == tyvar2
 748   = k subst
 749 uTysX (TyVarTy tyvar1) ty2 k subst@(tmpls,_)
 750   | tyvar1 `elemVarSet` tmpls
 751   = uVarX tyvar1 ty2 k subst
 752 uTysX ty1 (TyVarTy tyvar2) k subst@(tmpls,_)
 753   | tyvar2 `elemVarSet` tmpls
 754   = uVarX tyvar2 ty1 k subst
 755
 756         -- Predicates
 757 uTysX (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) k subst
 758   | n1 == n2 = uTysX t1 t2 k subst
 759 uTysX (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) k subst
 760   | c1 == c2 = uTyListsX tys1 tys2 k subst
 761 uTysX (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) k subst
 762   | tc1 == tc2 = uTyListsX tys1 tys2 k subst
 763
 764         -- Functions; just check the two parts
 765 uTysX (FunTy fun1 arg1) (FunTy fun2 arg2) k subst
 766   = uTysX fun1 fun2 (uTysX arg1 arg2 k) subst
 767
 768         -- Type constructors must match
 769 uTysX (TyConApp con1 tys1) (TyConApp con2 tys2) k subst
 770   | (con1 == con2 && length tys1 == length tys2)
 771   = uTyListsX tys1 tys2 k subst
 772
 773         -- Applications need a bit of care!
 774         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 775         -- NB: we've already dealt with type variables and Notes,
 776         -- so if one type is an App the other one jolly well better be too
 777 uTysX (AppTy s1 t1) ty2 k subst
 778   = case tcSplitAppTy_maybe ty2 of
 779       Just (s2, t2) -> uTysX s1 s2 (uTysX t1 t2 k) subst
 780       Nothing       -> Nothing    -- Fail
 781
 782 uTysX ty1 (AppTy s2 t2) k subst
 783   = case tcSplitAppTy_maybe ty1 of
 784       Just (s1, t1) -> uTysX s1 s2 (uTysX t1 t2 k) subst
 785       Nothing       -> Nothing    -- Fail
 786
 787         -- Not expecting for-alls in unification
 788 #ifdef DEBUG
 789 uTysX (ForAllTy _ _) ty2 k subst = panic "Unify.uTysX subst:ForAllTy (1st arg)"
 790 uTysX ty1 (ForAllTy _ _) k subst = panic "Unify.uTysX subst:ForAllTy (2nd arg)"
 791 #endif
 792
 793         -- Ignore usages
 794 uTysX (UsageTy _ t1) t2 k subst = uTysX t1 t2 k subst
 795 uTysX t1 (UsageTy _ t2) k subst = uTysX t1 t2 k subst
 796
 797         -- Anything else fails
 798 uTysX ty1 ty2 k subst = Nothing
 799
 800
 801 uTyListsX []         []         k subst = k subst
 802 uTyListsX (ty1:tys1) (ty2:tys2) k subst = uTysX ty1 ty2 (uTyListsX tys1 tys2 k) subst
 803 uTyListsX tys1       tys2       k subst = Nothing   -- Fail if the lists are different lengths
 804 \end{code}
 805
 806 \begin{code}
 807 -- Invariant: tv1 is a unifiable variable
 808 uVarX tv1 ty2 k subst@(tmpls, env)
 809   = case lookupSubstEnv env tv1 of
 810       Just (DoneTy ty1) ->    -- Already bound
 811                      uTysX ty1 ty2 k subst
 812
 813       Nothing        -- Not already bound
 814                |  typeKind ty2 `eqKind` tyVarKind tv1
 815                && occur_check_ok ty2
 816                ->     -- No kind mismatch nor occur check
 817                   UASSERT( not (isUTy ty2) )
 818                   k (tmpls, extendSubstEnv env tv1 (DoneTy ty2))
 819
 820                | otherwise -> Nothing   -- Fail if kind mis-match or occur check
 821   where
 822     occur_check_ok ty = all occur_check_ok_tv (varSetElems (tyVarsOfType ty))
 823     occur_check_ok_tv tv | tv1 == tv = False
 824                          | otherwise = case lookupSubstEnv env tv of
 825                                          Nothing           -> True
 826                                          Just (DoneTy ty)  -> occur_check_ok ty
 827 \end{code}
 828
 829
 830
 831 %************************************************************************
 832 %*                                                                      *
 833 \subsection{Matching on types}
 834 %*                                                                      *
 835 %************************************************************************
 836
 837 Matching is a {\em unidirectional} process, matching a type against a
 838 template (which is just a type with type variables in it).  The
 839 matcher assumes that there are no repeated type variables in the
 840 template, so that it simply returns a mapping of type variables to
 841 types.  It also fails on nested foralls.
 842
 843 @matchTys@ matches corresponding elements of a list of templates and
 844 types.  It and @matchTy@ both ignore usage annotations, unlike the
 845 main function @match@.
 846
 847 \begin{code}
 848 matchTy :: TyVarSet                     -- Template tyvars
 849         -> Type                         -- Template
 850         -> Type                         -- Proposed instance of template
 851         -> Maybe TyVarSubstEnv          -- Matching substitution
 852
 853
 854 matchTys :: TyVarSet                    -- Template tyvars
 855          -> [Type]                      -- Templates
 856          -> [Type]                      -- Proposed instance of template
 857          -> Maybe (TyVarSubstEnv,               -- Matching substitution
 858                    [Type])              -- Left over instance types
 859
 860 matchTy tmpls ty1 ty2 = match ty1 ty2 tmpls (\ senv -> Just senv) emptySubstEnv
 861
 862 matchTys tmpls tys1 tys2 = match_list tys1 tys2 tmpls
 863                                       (\ (senv,tys) -> Just (senv,tys))
 864                                       emptySubstEnv
 865 \end{code}
 866
 867 @match@ is the main function.  It takes a flag indicating whether
 868 usage annotations are to be respected.
 869
 870 \begin{code}
 871 match :: Type -> Type                           -- Current match pair
 872       -> TyVarSet                               -- Template vars
 873       -> (TyVarSubstEnv -> Maybe result)        -- Continuation
 874       -> TyVarSubstEnv                          -- Current subst
 875       -> Maybe result
 876
 877 -- When matching against a type variable, see if the variable
 878 -- has already been bound.  If so, check that what it's bound to
 879 -- is the same as ty; if not, bind it and carry on.
 880
 881 match (TyVarTy v) ty tmpls k senv
 882   | v `elemVarSet` tmpls
 883   =     -- v is a template variable
 884     case lookupSubstEnv senv v of
 885         Nothing -> UASSERT( not (isUTy ty) )
 886                    k (extendSubstEnv senv v (DoneTy ty))
 887         Just (DoneTy ty')  | ty' `tcEqType` ty   -> k senv   -- Succeeds
 888                            | otherwise           -> Nothing  -- Fails
 889
 890   | otherwise
 891   =     -- v is not a template variable; ty had better match
 892         -- Can't use (==) because types differ
 893     case tcGetTyVar_maybe ty of
 894         Just v' | v == v' -> k senv    -- Success
 895         other             -> Nothing   -- Failure
 896     -- This tcGetTyVar_maybe is *required* because it must strip Notes.
 897     -- I guess the reason the Note-stripping case is *last* rather than first
 898     -- is to preserve type synonyms etc., so I'm not moving it to the
 899     -- top; but this means that (without the deNotetype) a type
 900     -- variable may not match the pattern (TyVarTy v') as one would
 901     -- expect, due to an intervening Note.  KSW 2000-06.
 902
 903         -- Predicates
 904 match (SourceTy (IParam n1 t1)) (SourceTy (IParam n2 t2)) tmpls k senv
 905   | n1 == n2 = match t1 t2 tmpls k senv
 906 match (SourceTy (ClassP c1 tys1)) (SourceTy (ClassP c2 tys2)) tmpls k senv
 907   | c1 == c2 = match_list_exactly tys1 tys2 tmpls k senv
 908 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
 909   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
 910
 911         -- Functions; just check the two parts
 912 match (FunTy arg1 res1) (FunTy arg2 res2) tmpls k senv
 913   = match arg1 arg2 tmpls (match res1 res2 tmpls k) senv
 914
 915 match (AppTy fun1 arg1) ty2 tmpls k senv
 916   = case tcSplitAppTy_maybe ty2 of
 917         Just (fun2,arg2) -> match fun1 fun2 tmpls (match arg1 arg2 tmpls k) senv
 918         Nothing          -> Nothing     -- Fail
 919
 920 match (TyConApp tc1 tys1) (TyConApp tc2 tys2) tmpls k senv
 921   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
 922
 923 -- Newtypes are opaque; other source types should not happen
 924 match (SourceTy (NType tc1 tys1)) (SourceTy (NType tc2 tys2)) tmpls k senv
 925   | tc1 == tc2 = match_list_exactly tys1 tys2 tmpls k senv
 926
 927 match (UsageTy _ ty1) ty2 tmpls k senv = match ty1 ty2 tmpls k senv
 928 match ty1 (UsageTy _ ty2) tmpls k senv = match ty1 ty2 tmpls k senv
 929
 930         -- With type synonyms, we have to be careful for the exact
 931         -- same reasons as in the unifier.  Please see the
 932         -- considerable commentary there before changing anything
 933         -- here! (WDP 95/05)
 934 match (NoteTy n1 ty1) ty2      tmpls k senv = match ty1 ty2 tmpls k senv
 935 match ty1      (NoteTy n2 ty2) tmpls k senv = match ty1 ty2 tmpls k senv
 936
 937 -- Catch-all fails
 938 match _ _ _ _ _ = Nothing
 939
 940 match_list_exactly tys1 tys2 tmpls k senv
 941   = match_list tys1 tys2 tmpls k' senv
 942   where
 943     k' (senv', tys2') | null tys2' = k senv'    -- Succeed
 944                       | otherwise  = Nothing    -- Fail
 945
 946 match_list []         tys2       tmpls k senv = k (senv, tys2)
 947 match_list (ty1:tys1) []         tmpls k senv = Nothing -- Not enough arg tys => failure
 948 match_list (ty1:tys1) (ty2:tys2) tmpls k senv
 949   = match ty1 ty2 tmpls (match_list tys1 tys2 tmpls k) senv
 950 \end{code}