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