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