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