ghc/compiler/typecheck/TcMType.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section{Monadic type operations}
   5
   6 This module contains monadic operations over types that contain mutable type variables
   7
   8 \begin{code}
   9 module TcMType (
  10   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcRhoType, TcTyVarSet,
  11
  12   --------------------------------
  13   -- Creating new mutable type variables
  14   newTyVar,
  15   newTyVarTy,           -- Kind -> NF_TcM TcType
  16   newTyVarTys,          -- Int -> Kind -> NF_TcM [TcType]
  17   newKindVar, newKindVars, newBoxityVar,
  18
  19   --------------------------------
  20   -- Instantiation
  21   tcInstTyVar, tcInstTyVars,
  22   tcInstSigVars, tcInstType,
  23   tcSplitRhoTyM,
  24
  25   --------------------------------
  26   -- Checking type validity
  27   Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
  28   SourceTyCtxt(..), checkValidTheta,
  29
  30   --------------------------------
  31   -- Unification
  32   unifyTauTy, unifyTauTyList, unifyTauTyLists,
  33   unifyFunTy, unifyListTy, unifyTupleTy,
  34   unifyKind, unifyKinds, unifyOpenTypeKind,
  35
  36   --------------------------------
  37   -- Zonking
  38   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
  39   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
  40   zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
  41
  42   ) where
  43
  44 #include "HsVersions.h"
  45
  46
  47 -- friends:
  48 import TypeRep          ( Type(..), SourceType(..), TyNote(..),  -- Friend; can see representation
  49                           Kind, TauType, ThetaType,
  50                           openKindCon, typeCon
  51                         )
  52 import TcType           ( tcEqType, tcCmpPred,
  53                           tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
  54                           tcSplitTyConApp_maybe, tcSplitFunTy_maybe, tcSplitForAllTys,
  55                           tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, isUnLiftedType, isIPPred,
  56
  57                           mkAppTy, mkTyVarTy, mkTyVarTys, mkFunTy, mkTyConApp,
  58                           tyVarsOfPred,
  59
  60                           liftedTypeKind, unliftedTypeKind, openTypeKind, defaultKind, superKind,
  61                           superBoxity, liftedBoxity, hasMoreBoxityInfo, typeKind,
  62                           tyVarsOfType, tyVarsOfTypes, tidyOpenType, tidyOpenTypes, tidyTyVar,
  63                           eqKind, isTypeKind
  64                         )
  65 import Subst            ( Subst, mkTopTyVarSubst, substTy )
  66 import Class            ( classArity, className )
  67 import TyCon            ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon,
  68                           isTupleTyCon, tyConArity, tupleTyConBoxity, tyConName )
  69 import PrimRep          ( PrimRep(VoidRep) )
  70 import Var              ( TyVar, varName, tyVarKind, tyVarName, isTyVar, mkTyVar,
  71                           isMutTyVar, isSigTyVar )
  72
  73 -- others:
  74 import TcMonad          -- TcType, amongst others
  75 import TysWiredIn       ( voidTy, listTyCon, mkListTy, mkTupleTy )
  76 import FunDeps          ( grow )
  77 import PprType          ( pprPred, pprSourceType, pprTheta )
  78 import Name             ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
  79                           mkLocalName, mkDerivedTyConOcc, isSystemName
  80                         )
  81 import VarSet
  82 import BasicTypes       ( Boxity, Arity, isBoxed )
  83 import CmdLineOpts      ( dopt, DynFlag(..) )
  84 import Unique           ( Uniquable(..) )
  85 import SrcLoc           ( noSrcLoc )
  86 import Util             ( nOfThem )
  87 import ListSetOps       ( removeDups )
  88 import Outputable
  89 \end{code}
  90
  91
  92 %************************************************************************
  93 %*                                                                      *
  94 \subsection{New type variables}
  95 %*                                                                      *
  96 %************************************************************************
  97
  98 \begin{code}
  99 newTyVar :: Kind -> NF_TcM TcTyVar
 100 newTyVar kind
 101   = tcGetUnique         `thenNF_Tc` \ uniq ->
 102     tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
 103
 104 newTyVarTy  :: Kind -> NF_TcM TcType
 105 newTyVarTy kind
 106   = newTyVar kind       `thenNF_Tc` \ tc_tyvar ->
 107     returnNF_Tc (TyVarTy tc_tyvar)
 108
 109 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
 110 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 111
 112 newKindVar :: NF_TcM TcKind
 113 newKindVar
 114   = tcGetUnique                                                 `thenNF_Tc` \ uniq ->
 115     tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind     `thenNF_Tc` \ kv ->
 116     returnNF_Tc (TyVarTy kv)
 117
 118 newKindVars :: Int -> NF_TcM [TcKind]
 119 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 120
 121 newBoxityVar :: NF_TcM TcKind
 122 newBoxityVar
 123   = tcGetUnique                                                 `thenNF_Tc` \ uniq ->
 124     tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity  `thenNF_Tc` \ kv ->
 125     returnNF_Tc (TyVarTy kv)
 126 \end{code}
 127
 128
 129 %************************************************************************
 130 %*                                                                      *
 131 \subsection{Type instantiation}
 132 %*                                                                      *
 133 %************************************************************************
 134
 135 I don't understand why this is needed
 136 An old comments says "No need for tcSplitForAllTyM because a type
 137         variable can't be instantiated to a for-all type"
 138 But the same is true of rho types!
 139
 140 \begin{code}
 141 tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
 142 tcSplitRhoTyM t
 143   = go t t []
 144  where
 145         -- A type variable is never instantiated to a dictionary type,
 146         -- so we don't need to do a tcReadVar on the "arg".
 147     go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
 148                                         Just pair -> go res res (pair:ts)
 149                                         Nothing   -> returnNF_Tc (reverse ts, syn_t)
 150     go syn_t (NoteTy n t)    ts = go syn_t t ts
 151     go syn_t (TyVarTy tv)    ts = getTcTyVar tv         `thenNF_Tc` \ maybe_ty ->
 152                                   case maybe_ty of
 153                                     Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
 154                                     other                          -> returnNF_Tc (reverse ts, syn_t)
 155     go syn_t (UsageTy _ t)   ts = go syn_t t ts
 156     go syn_t t               ts = returnNF_Tc (reverse ts, syn_t)
 157 \end{code}
 158
 159
 160 %************************************************************************
 161 %*                                                                      *
 162 \subsection{Type instantiation}
 163 %*                                                                      *
 164 %************************************************************************
 165
 166 Instantiating a bunch of type variables
 167
 168 \begin{code}
 169 tcInstTyVars :: [TyVar]
 170              -> NF_TcM ([TcTyVar], [TcType], Subst)
 171
 172 tcInstTyVars tyvars
 173   = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
 174     let
 175         tys = mkTyVarTys tc_tyvars
 176     in
 177     returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
 178                 -- Since the tyvars are freshly made,
 179                 -- they cannot possibly be captured by
 180                 -- any existing for-alls.  Hence mkTopTyVarSubst
 181
 182 tcInstTyVar tyvar
 183   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 184     let
 185         name = setNameUnique (tyVarName tyvar) uniq
 186         -- Note that we don't change the print-name
 187         -- This won't confuse the type checker but there's a chance
 188         -- that two different tyvars will print the same way
 189         -- in an error message.  -dppr-debug will show up the difference
 190         -- Better watch out for this.  If worst comes to worst, just
 191         -- use mkSysLocalName.
 192     in
 193     tcNewMutTyVar name (tyVarKind tyvar)
 194
 195 tcInstSigVars tyvars    -- Very similar to tcInstTyVar
 196   = tcGetUniques        `thenNF_Tc` \ uniqs ->
 197     listTc [ ASSERT( not (kind `eqKind` openTypeKind) ) -- Shouldn't happen
 198              tcNewSigTyVar name kind
 199            | (tyvar, uniq) <- tyvars `zip` uniqs,
 200              let name = setNameUnique (tyVarName tyvar) uniq,
 201              let kind = tyVarKind tyvar
 202            ]
 203 \end{code}
 204
 205 @tcInstType@ instantiates the outer-level for-alls of a TcType with
 206 fresh type variables, splits off the dictionary part, and returns the results.
 207
 208 \begin{code}
 209 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
 210 tcInstType ty
 211   = case tcSplitForAllTys ty of
 212         ([],     rho) ->        -- There may be overloading but no type variables;
 213                                 --      (?x :: Int) => Int -> Int
 214                          let
 215                            (theta, tau) = tcSplitRhoTy rho      -- Used to be tcSplitRhoTyM
 216                          in
 217                          returnNF_Tc ([], theta, tau)
 218
 219         (tyvars, rho) -> tcInstTyVars tyvars                    `thenNF_Tc` \ (tyvars', _, tenv)  ->
 220                          let
 221                            (theta, tau) = tcSplitRhoTy (substTy tenv rho)       -- Used to be tcSplitRhoTyM
 222                          in
 223                          returnNF_Tc (tyvars', theta, tau)
 224 \end{code}
 225
 226
 227
 228 %************************************************************************
 229 %*                                                                      *
 230 \subsection{Putting and getting  mutable type variables}
 231 %*                                                                      *
 232 %************************************************************************
 233
 234 \begin{code}
 235 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
 236 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
 237 \end{code}
 238
 239 Putting is easy:
 240
 241 \begin{code}
 242 putTcTyVar tyvar ty
 243   | not (isMutTyVar tyvar)
 244   = pprTrace "putTcTyVar" (ppr tyvar) $
 245     returnNF_Tc ty
 246
 247   | otherwise
 248   = ASSERT( isMutTyVar tyvar )
 249     UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
 250     tcWriteMutTyVar tyvar (Just ty)     `thenNF_Tc_`
 251     returnNF_Tc ty
 252 \end{code}
 253
 254 Getting is more interesting.  The easy thing to do is just to read, thus:
 255
 256 \begin{verbatim}
 257 getTcTyVar tyvar = tcReadMutTyVar tyvar
 258 \end{verbatim}
 259
 260 But it's more fun to short out indirections on the way: If this
 261 version returns a TyVar, then that TyVar is unbound.  If it returns
 262 any other type, then there might be bound TyVars embedded inside it.
 263
 264 We return Nothing iff the original box was unbound.
 265
 266 \begin{code}
 267 getTcTyVar tyvar
 268   | not (isMutTyVar tyvar)
 269   = pprTrace "getTcTyVar" (ppr tyvar) $
 270     returnNF_Tc (Just (mkTyVarTy tyvar))
 271
 272   | otherwise
 273   = ASSERT2( isMutTyVar tyvar, ppr tyvar )
 274     tcReadMutTyVar tyvar                                `thenNF_Tc` \ maybe_ty ->
 275     case maybe_ty of
 276         Just ty -> short_out ty                         `thenNF_Tc` \ ty' ->
 277                    tcWriteMutTyVar tyvar (Just ty')     `thenNF_Tc_`
 278                    returnNF_Tc (Just ty')
 279
 280         Nothing    -> returnNF_Tc Nothing
 281
 282 short_out :: TcType -> NF_TcM TcType
 283 short_out ty@(TyVarTy tyvar)
 284   | not (isMutTyVar tyvar)
 285   = returnNF_Tc ty
 286
 287   | otherwise
 288   = tcReadMutTyVar tyvar        `thenNF_Tc` \ maybe_ty ->
 289     case maybe_ty of
 290         Just ty' -> short_out ty'                       `thenNF_Tc` \ ty' ->
 291                     tcWriteMutTyVar tyvar (Just ty')    `thenNF_Tc_`
 292                     returnNF_Tc ty'
 293
 294         other    -> returnNF_Tc ty
 295
 296 short_out other_ty = returnNF_Tc other_ty
 297 \end{code}
 298
 299
 300 %************************************************************************
 301 %*                                                                      *
 302 \subsection{Zonking -- the exernal interfaces}
 303 %*                                                                      *
 304 %************************************************************************
 305
 306 -----------------  Type variables
 307
 308 \begin{code}
 309 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
 310 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
 311
 312 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
 313 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars  `thenNF_Tc` \ tys ->
 314                            returnNF_Tc (tyVarsOfTypes tys)
 315
 316 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
 317 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
 318
 319 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
 320 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
 321 -- Usually this job is done by checkSigTyVars, but in a couple of places
 322 -- that is overkill, so we use this simpler chap
 323 zonkTcSigTyVars tyvars
 324   = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
 325     returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
 326 \end{code}
 327
 328 -----------------  Types
 329
 330 \begin{code}
 331 zonkTcType :: TcType -> NF_TcM TcType
 332 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
 333
 334 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
 335 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 336
 337 zonkTcClassConstraints cts = mapNF_Tc zonk cts
 338     where zonk (clas, tys)
 339             = zonkTcTypes tys   `thenNF_Tc` \ new_tys ->
 340               returnNF_Tc (clas, new_tys)
 341
 342 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
 343 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
 344
 345 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
 346 zonkTcPredType (ClassP c ts) =
 347     zonkTcTypes ts      `thenNF_Tc` \ new_ts ->
 348     returnNF_Tc (ClassP c new_ts)
 349 zonkTcPredType (IParam n t) =
 350     zonkTcType t        `thenNF_Tc` \ new_t ->
 351     returnNF_Tc (IParam n new_t)
 352 \end{code}
 353
 354 -------------------  These ...ToType, ...ToKind versions
 355                      are used at the end of type checking
 356
 357 \begin{code}
 358 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
 359 zonkKindEnv pairs
 360   = mapNF_Tc zonk_it pairs
 361  where
 362     zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
 363                               returnNF_Tc (name, kind)
 364
 365         -- When zonking a kind, we want to
 366         --      zonk a *kind* variable to (Type *)
 367         --      zonk a *boxity* variable to *
 368     zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind   = putTcTyVar kv liftedTypeKind
 369                              | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
 370                              | otherwise                         = pprPanic "zonkKindEnv" (ppr kv)
 371
 372 zonkTcTypeToType :: TcType -> NF_TcM Type
 373 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
 374   where
 375         -- Zonk a mutable but unbound type variable to
 376         --      Void            if it has kind Lifted
 377         --      :Void           otherwise
 378         -- We know it's unbound even though we don't carry an environment,
 379         -- because at the binding site for a type variable we bind the
 380         -- mutable tyvar to a fresh immutable one.  So the mutable store
 381         -- plays the role of an environment.  If we come across a mutable
 382         -- type variable that isn't so bound, it must be completely free.
 383     zonk_unbound_tyvar tv
 384         | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
 385         = putTcTyVar tv voidTy  -- Just to avoid creating a new tycon in
 386                                 -- this vastly common case
 387         | otherwise
 388         = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
 389         where
 390           kind = tyVarKind tv
 391
 392     mk_void_tycon tv kind       -- Make a new TyCon with the same kind as the
 393                                 -- type variable tv.  Same name too, apart from
 394                                 -- making it start with a colon (sigh)
 395                 -- I dread to think what will happen if this gets out into an
 396                 -- interface file.  Catastrophe likely.  Major sigh.
 397         = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
 398           mkPrimTyCon tc_name kind 0 [] VoidRep
 399         where
 400           tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
 401
 402 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
 403 -- of a type variable, at the *end* of type checking.  It changes
 404 -- the *mutable* type variable into an *immutable* one.
 405 --
 406 -- It does this by making an immutable version of tv and binds tv to it.
 407 -- Now any bound occurences of the original type variable will get
 408 -- zonked to the immutable version.
 409
 410 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
 411 zonkTcTyVarToTyVar tv
 412   = let
 413                 -- Make an immutable version, defaulting
 414                 -- the kind to lifted if necessary
 415         immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
 416         immut_tv_ty = mkTyVarTy immut_tv
 417
 418         zap tv = putTcTyVar tv immut_tv_ty
 419                 -- Bind the mutable version to the immutable one
 420     in
 421         -- If the type variable is mutable, then bind it to immut_tv_ty
 422         -- so that all other occurrences of the tyvar will get zapped too
 423     zonkTyVar zap tv            `thenNF_Tc` \ ty2 ->
 424
 425     WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
 426
 427     returnNF_Tc immut_tv
 428 \end{code}
 429
 430
 431 %************************************************************************
 432 %*                                                                      *
 433 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 434 %*                                                                      *
 435 %*              For internal use only!                                  *
 436 %*                                                                      *
 437 %************************************************************************
 438
 439 \begin{code}
 440 -- zonkType is used for Kinds as well
 441
 442 -- For unbound, mutable tyvars, zonkType uses the function given to it
 443 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 444 --      type variable and zonks the kind too
 445
 446 zonkType :: (TcTyVar -> NF_TcM Type)    -- What to do with unbound mutable type variables
 447                                         -- see zonkTcType, and zonkTcTypeToType
 448          -> TcType
 449          -> NF_TcM Type
 450 zonkType unbound_var_fn ty
 451   = go ty
 452   where
 453     go (TyConApp tycon tys)       = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 454                                     returnNF_Tc (TyConApp tycon tys')
 455
 456     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenNF_Tc` \ ty1' ->
 457                                     go ty2              `thenNF_Tc` \ ty2' ->
 458                                     returnNF_Tc (NoteTy (SynNote ty1') ty2')
 459
 460     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
 461
 462     go (SourceTy p)               = go_pred p           `thenNF_Tc` \ p' ->
 463                                     returnNF_Tc (SourceTy p')
 464
 465     go (FunTy arg res)            = go arg              `thenNF_Tc` \ arg' ->
 466                                     go res              `thenNF_Tc` \ res' ->
 467                                     returnNF_Tc (FunTy arg' res')
 468
 469     go (AppTy fun arg)            = go fun              `thenNF_Tc` \ fun' ->
 470                                     go arg              `thenNF_Tc` \ arg' ->
 471                                     returnNF_Tc (mkAppTy fun' arg')
 472
 473     go (UsageTy u ty)             = go u                `thenNF_Tc` \ u'  ->
 474                                     go ty               `thenNF_Tc` \ ty' ->
 475                                     returnNF_Tc (UsageTy u' ty')
 476
 477         -- The two interesting cases!
 478     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
 479
 480     go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar   `thenNF_Tc` \ tyvar' ->
 481                              go ty                      `thenNF_Tc` \ ty' ->
 482                              returnNF_Tc (ForAllTy tyvar' ty')
 483
 484     go_pred (ClassP c tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
 485                              returnNF_Tc (ClassP c tys')
 486     go_pred (NType tc tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
 487                              returnNF_Tc (NType tc tys')
 488     go_pred (IParam n ty) = go ty               `thenNF_Tc` \ ty' ->
 489                             returnNF_Tc (IParam n ty')
 490
 491 zonkTyVar :: (TcTyVar -> NF_TcM Type)           -- What to do for an unbound mutable variable
 492           -> TcTyVar -> NF_TcM TcType
 493 zonkTyVar unbound_var_fn tyvar
 494   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
 495                                 -- zonking a forall type, when the bound type variable
 496                                 -- needn't be mutable
 497   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
 498     returnNF_Tc (TyVarTy tyvar)
 499
 500   | otherwise
 501   =  getTcTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 502      case maybe_ty of
 503           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
 504           Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
 505 \end{code}
 506
 507
 508
 509 %************************************************************************
 510 %*                                                                      *
 511 \subsection{Checking a user type}
 512 %*                                                                      *
 513 %************************************************************************
 514
 515 When dealing with a user-written type, we first translate it from an HsType
 516 to a Type, performing kind checking, and then check various things that should
 517 be true about it.  We don't want to perform these checks at the same time
 518 as the initial translation because (a) they are unnecessary for interface-file
 519 types and (b) when checking a mutually recursive group of type and class decls,
 520 we can't "look" at the tycons/classes yet.
 521
 522 One thing we check for is 'rank'.
 523
 524         Rank 0:         monotypes (no foralls)
 525         Rank 1:         foralls at the front only, Rank 0 inside
 526         Rank 2:         foralls at the front, Rank 1 on left of fn arrow,
 527
 528         basic ::= tyvar | T basic ... basic
 529
 530         r2  ::= forall tvs. cxt => r2a
 531         r2a ::= r1 -> r2a | basic
 532         r1  ::= forall tvs. cxt => r0
 533         r0  ::= r0 -> r0 | basic
 534
 535
 536 \begin{code}
 537 data UserTypeCtxt
 538   = FunSigCtxt Name     -- Function type signature
 539   | ExprSigCtxt         -- Expression type signature
 540   | ConArgCtxt Name     -- Data constructor argument
 541   | TySynCtxt Name      -- RHS of a type synonym decl
 542   | GenPatCtxt          -- Pattern in generic decl
 543                         --      f{| a+b |} (Inl x) = ...
 544   | PatSigCtxt          -- Type sig in pattern
 545                         --      f (x::t) = ...
 546   | ResSigCtxt          -- Result type sig
 547                         --      f x :: t = ....
 548   | ForSigCtxt Name     -- Foreign inport or export signature
 549   | RuleSigCtxt Name    -- Signature on a forall'd variable in a RULE
 550
 551 pprUserTypeCtxt (FunSigCtxt n)  = ptext SLIT("the type signature for") <+> quotes (ppr n)
 552 pprUserTypeCtxt ExprSigCtxt     = ptext SLIT("an expression type signature")
 553 pprUserTypeCtxt (ConArgCtxt c)  = ptext SLIT("the type of constructor") <+> quotes (ppr c)
 554 pprUserTypeCtxt (TySynCtxt c)   = ptext SLIT("the RHS of a type synonym declaration") <+> quotes (ppr c)
 555 pprUserTypeCtxt GenPatCtxt      = ptext SLIT("the type pattern of a generic definition")
 556 pprUserTypeCtxt PatSigCtxt      = ptext SLIT("a pattern type signature")
 557 pprUserTypeCtxt ResSigCtxt      = ptext SLIT("a result type signature")
 558 pprUserTypeCtxt (ForSigCtxt n)  = ptext SLIT("the foreign signature for") <+> quotes (ppr n)
 559 pprUserTypeCtxt (RuleSigCtxt n) = ptext SLIT("the type signature on") <+> quotes (ppr n)
 560 \end{code}
 561
 562 \begin{code}
 563 checkValidType :: UserTypeCtxt -> Type -> TcM ()
 564 -- Checks that the type is valid for the given context
 565 checkValidType ctxt ty
 566   = doptsTc Opt_GlasgowExts     `thenNF_Tc` \ gla_exts ->
 567     let
 568         rank = case ctxt of
 569                  GenPatCtxt               -> 0
 570                  PatSigCtxt               -> 0
 571                  ResSigCtxt               -> 0
 572                  ExprSigCtxt              -> 1
 573                  FunSigCtxt _ | gla_exts  -> 2
 574                               | otherwise -> 1
 575                  ConArgCtxt _ | gla_exts  -> 2  -- We are given the type of the entire
 576                               | otherwise -> 1  -- constructor; hence rank 1 is ok
 577                  TySynCtxt _  | gla_exts  -> 1
 578                               | otherwise -> 0
 579                  ForSigCtxt _             -> 1
 580                  RuleSigCtxt _            -> 1
 581
 582         actual_kind = typeKind ty
 583
 584         actual_kind_is_lifted = actual_kind `eqKind` liftedTypeKind
 585
 586         kind_ok = case ctxt of
 587                         TySynCtxt _  -> True    -- Any kind will do
 588                         GenPatCtxt   -> actual_kind_is_lifted
 589                         ForSigCtxt _ -> actual_kind_is_lifted
 590                         other        -> isTypeKind actual_kind
 591     in
 592     tcAddErrCtxt (checkTypeCtxt ctxt ty)        $
 593
 594         -- Check that the thing has kind Type, and is lifted if necessary
 595     checkTc kind_ok (kindErr actual_kind)       `thenTc_`
 596
 597         -- Check the internal validity of the type itself
 598     check_poly_type rank ty
 599
 600 -- Notes re TySynCtxt
 601 -- We allow type synonyms that aren't types; e.g.  type List = []
 602 --
 603 -- If the RHS mentions tyvars that aren't in scope, we'll
 604 -- quantify over them:
 605 --      e.g.    type T = a->a
 606 -- will become  type T = forall a. a->a
 607 --
 608 -- With gla-exts that's right, but for H98 we should complain.
 609
 610
 611 ----------------------------------------
 612 type Rank = Int
 613 check_poly_type :: Rank -> Type -> TcM ()
 614 check_poly_type rank ty
 615   | rank == 0
 616   = check_tau_type 0 False ty
 617   | otherwise   -- rank > 0
 618   = let
 619         (tvs, theta, tau) = tcSplitSigmaTy ty
 620     in
 621     check_valid_theta SigmaCtxt theta   `thenTc_`
 622     check_tau_type (rank-1) False tau   `thenTc_`
 623     checkAmbiguity tvs theta tau
 624
 625 ----------------------------------------
 626 check_arg_type :: Type -> TcM ()
 627 -- The sort of type that can instantiate a type variable,
 628 -- or be the argument of a type constructor.
 629 -- Not an unboxed tuple, not a forall.
 630 -- Other unboxed types are very occasionally allowed as type
 631 -- arguments depending on the kind of the type constructor
 632 --
 633 -- For example, we want to reject things like:
 634 --
 635 --      instance Ord a => Ord (forall s. T s a)
 636 -- and
 637 --      g :: T s (forall b.b)
 638 --
 639 -- NB: unboxed tuples can have polymorphic or unboxed args.
 640 --     This happens in the workers for functions returning
 641 --     product types with polymorphic components.
 642 --     But not in user code
 643 --
 644 -- Question: what about nested unboxed tuples?
 645 --           Currently rejected.
 646 check_arg_type ty
 647   = check_tau_type 0 False ty   `thenTc_`
 648     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 649
 650 ----------------------------------------
 651 check_tau_type :: Rank -> Bool -> Type -> TcM ()
 652 -- Rank is allowed rank for function args
 653 -- No foralls otherwise
 654 -- Bool is True iff unboxed tuple are allowed here
 655
 656 check_tau_type rank ubx_tup_ok ty@(UsageTy _ _)  = addErrTc (usageTyErr ty)
 657 check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = addErrTc (forAllTyErr ty)
 658 check_tau_type rank ubx_tup_ok (SourceTy sty)    = getDOptsTc           `thenNF_Tc` \ dflags ->
 659                                                    check_source_ty dflags TypeCtxt sty
 660 check_tau_type rank ubx_tup_ok (TyVarTy _)       = returnTc ()
 661 check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
 662   = check_poly_type rank      arg_ty    `thenTc_`
 663     check_tau_type  rank True res_ty
 664
 665 check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
 666   = check_arg_type ty1 `thenTc_` check_arg_type ty2
 667
 668 check_tau_type rank ubx_tup_ok (NoteTy note ty)
 669   = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
 670
 671 check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
 672   | isSynTyCon tc
 673   = checkTc syn_arity_ok arity_msg      `thenTc_`
 674     mapTc_ check_arg_type tys
 675
 676   | isUnboxedTupleTyCon tc
 677   = checkTc ubx_tup_ok ubx_tup_msg      `thenTc_`
 678     mapTc_ (check_tau_type 0 True) tys          -- Args are allowed to be unlifted, or
 679                                                 -- more unboxed tuples, so can't use check_arg_ty
 680
 681   | otherwise
 682   = mapTc_ check_arg_type tys
 683
 684   where
 685     syn_arity_ok = tc_arity <= n_args
 686                 -- It's OK to have an *over-applied* type synonym
 687                 --      data Tree a b = ...
 688                 --      type Foo a = Tree [a]
 689                 --      f :: Foo a b -> ...
 690     n_args    = length tys
 691     tc_arity  = tyConArity tc
 692
 693     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
 694     ubx_tup_msg = ubxArgTyErr ty
 695
 696 ----------------------------------------
 697 check_note (FTVNote _)  = returnTc ()
 698 check_note (SynNote ty) = check_tau_type 0 False ty
 699 \end{code}
 700
 701
 702 \begin{code}
 703 data SourceTyCtxt
 704   = ClassSCCtxt Name    -- Superclasses of clas
 705   | SigmaCtxt           -- Context of a normal for-all type
 706   | DataTyCtxt Name     -- Context of a data decl
 707   | TypeCtxt            -- Source type in an ordinary type
 708   | InstDeclCtxt        -- Context of an instance decl
 709
 710 pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
 711 pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
 712 pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
 713 pprSourceTyCtxt InstDeclCtxt    = ptext SLIT("the context of an instance declaration")
 714 pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
 715 \end{code}
 716
 717 \begin{code}
 718 checkValidTheta :: SourceTyCtxt -> ThetaType -> TcM ()
 719 checkValidTheta ctxt theta
 720   = tcAddErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 721
 722 -------------------------
 723 check_valid_theta ctxt []
 724   = returnTc ()
 725 check_valid_theta ctxt theta
 726   = getDOptsTc                                  `thenNF_Tc` \ dflags ->
 727     warnTc (not (null dups)) (dupPredWarn dups) `thenNF_Tc_`
 728     mapTc_ (check_source_ty dflags ctxt) theta
 729   where
 730     (_,dups) = removeDups tcCmpPred theta
 731
 732 -------------------------
 733 check_source_ty dflags ctxt pred@(ClassP cls tys)
 734   =     -- Class predicates are valid in all contexts
 735     mapTc_ check_arg_type tys                   `thenTc_`
 736     checkTc (arity == n_tys) arity_err          `thenTc_`
 737     checkTc (all tyvar_head tys || arby_preds_ok) (predTyVarErr pred)
 738
 739   where
 740     class_name = className cls
 741     arity      = classArity cls
 742     n_tys      = length tys
 743     arity_err  = arityErr "Class" class_name arity n_tys
 744
 745     arby_preds_ok = case ctxt of
 746                         InstDeclCtxt -> dopt Opt_AllowUndecidableInstances dflags
 747                         other        -> dopt Opt_GlasgowExts               dflags
 748
 749 check_source_ty dflags SigmaCtxt (IParam name ty) = check_arg_type ty
 750 check_source_ty dflags TypeCtxt  (NType tc tys)   = mapTc_ check_arg_type tys
 751
 752 -- Catch-all
 753 check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
 754
 755 -------------------------
 756 tyvar_head ty                   -- Haskell 98 allows predicates of form
 757   | tcIsTyVarTy ty = True       --      C (a ty1 .. tyn)
 758   | otherwise                   -- where a is a type variable
 759   = case tcSplitAppTy_maybe ty of
 760         Just (ty, _) -> tyvar_head ty
 761         Nothing      -> False
 762 \end{code}
 763
 764 Check for ambiguity
 765 ~~~~~~~~~~~~~~~~~~~
 766           forall V. P => tau
 767 is ambiguous if P contains generic variables
 768 (i.e. one of the Vs) that are not mentioned in tau
 769
 770 However, we need to take account of functional dependencies
 771 when we speak of 'mentioned in tau'.  Example:
 772         class C a b | a -> b where ...
 773 Then the type
 774         forall x y. (C x y) => x
 775 is not ambiguous because x is mentioned and x determines y
 776
 777 NOTE: In addition, GHC insists that at least one type variable
 778 in each constraint is in V.  So we disallow a type like
 779         forall a. Eq b => b -> b
 780 even in a scope where b is in scope.
 781 This is the is_free test below.
 782
 783 NB; the ambiguity check is only used for *user* types, not for types
 784 coming from inteface files.  The latter can legitimately have
 785 ambiguous types. Example
 786
 787    class S a where s :: a -> (Int,Int)
 788    instance S Char where s _ = (1,1)
 789    f:: S a => [a] -> Int -> (Int,Int)
 790    f (_::[a]) x = (a*x,b)
 791         where (a,b) = s (undefined::a)
 792
 793 Here the worker for f gets the type
 794         fw :: forall a. S a => Int -> (# Int, Int #)
 795
 796 If the list of tv_names is empty, we have a monotype, and then we
 797 don't need to check for ambiguity either, because the test can't fail
 798 (see is_ambig).
 799
 800 \begin{code}
 801 checkAmbiguity :: [TyVar] -> ThetaType -> TauType -> TcM ()
 802 checkAmbiguity forall_tyvars theta tau
 803   = mapTc_ check_pred theta     `thenTc_`
 804     returnTc ()
 805   where
 806     tau_vars          = tyVarsOfType tau
 807     extended_tau_vars = grow theta tau_vars
 808
 809     is_ambig ct_var   = (ct_var `elem` forall_tyvars) &&
 810                         not (ct_var `elemVarSet` extended_tau_vars)
 811     is_free ct_var    = not (ct_var `elem` forall_tyvars)
 812
 813     check_pred pred = checkTc (not any_ambig)                 (ambigErr pred) `thenTc_`
 814                       checkTc (isIPPred pred || not all_free) (freeErr  pred)
 815              where
 816                 ct_vars   = varSetElems (tyVarsOfPred pred)
 817                 all_free  = all is_free ct_vars
 818                 any_ambig = any is_ambig ct_vars
 819 \end{code}
 820
 821
 822 \begin{code}
 823 ambigErr pred
 824   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
 825          nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
 826                  ptext SLIT("must be reachable from the type after the =>"))]
 827
 828 freeErr pred
 829   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
 830                    ptext SLIT("are already in scope"),
 831          nest 4 (ptext SLIT("At least one must be universally quantified here"))
 832     ]
 833
 834 forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
 835 usageTyErr      ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
 836 unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
 837 ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
 838 badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprSourceType sty
 839 predTyVarErr pred  = ptext SLIT("Non-type variables in constraint:") <+> pprPred pred
 840 kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 841 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 842
 843 checkTypeCtxt ctxt ty
 844   = vcat [ptext SLIT("In the type:") <+> ppr_ty ty,
 845           ptext SLIT("While checking") <+> pprUserTypeCtxt ctxt ]
 846
 847         -- Hack alert.  If there are no tyvars, (ppr sigma_ty) will print
 848         -- something strange like {Eq k} -> k -> k, because there is no
 849         -- ForAll at the top of the type.  Since this is going to the user
 850         -- we want it to look like a proper Haskell type even then; hence the hack
 851         --
 852         -- This shows up in the complaint about
 853         --      case C a where
 854         --        op :: Eq a => a -> a
 855 ppr_ty ty | null forall_tvs && not (null theta) = pprTheta theta <+> ptext SLIT("=>") <+> ppr tau
 856           | otherwise                        = ppr ty
 857           where
 858             (forall_tvs, theta, tau) = tcSplitSigmaTy ty
 859
 860 checkThetaCtxt ctxt theta
 861   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
 862           ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 863 \end{code}
 864
 865
 866 %************************************************************************
 867 %*                                                                      *
 868 \subsection{Kind unification}
 869 %*                                                                      *
 870 %************************************************************************
 871
 872 \begin{code}
 873 unifyKind :: TcKind                 -- Expected
 874           -> TcKind                 -- Actual
 875           -> TcM ()
 876 unifyKind k1 k2
 877   = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
 878     uTys k1 k1 k2 k2
 879
 880 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
 881 unifyKinds []       []       = returnTc ()
 882 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2  `thenTc_`
 883                                unifyKinds ks1 ks2
 884 unifyKinds _ _ = panic "unifyKinds: length mis-match"
 885 \end{code}
 886
 887 \begin{code}
 888 unifyOpenTypeKind :: TcKind -> TcM ()
 889 -- Ensures that the argument kind is of the form (Type bx)
 890 -- for some boxity bx
 891
 892 unifyOpenTypeKind ty@(TyVarTy tyvar)
 893   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 894     case maybe_ty of
 895         Just ty' -> unifyOpenTypeKind ty'
 896         other    -> unify_open_kind_help ty
 897
 898 unifyOpenTypeKind ty
 899   | isTypeKind ty = returnTc ()
 900   | otherwise     = unify_open_kind_help ty
 901
 902 unify_open_kind_help ty -- Revert to ordinary unification
 903   = newBoxityVar        `thenNF_Tc` \ boxity ->
 904     unifyKind ty (mkTyConApp typeCon [boxity])
 905 \end{code}
 906
 907
 908 %************************************************************************
 909 %*                                                                      *
 910 \subsection[Unify-exported]{Exported unification functions}
 911 %*                                                                      *
 912 %************************************************************************
 913
 914 The exported functions are all defined as versions of some
 915 non-exported generic functions.
 916
 917 Unify two @TauType@s.  Dead straightforward.
 918
 919 \begin{code}
 920 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
 921 unifyTauTy ty1 ty2      -- ty1 expected, ty2 inferred
 922   = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
 923     uTys ty1 ty1 ty2 ty2
 924 \end{code}
 925
 926 @unifyTauTyList@ unifies corresponding elements of two lists of
 927 @TauType@s.  It uses @uTys@ to do the real work.  The lists should be
 928 of equal length.  We charge down the list explicitly so that we can
 929 complain if their lengths differ.
 930
 931 \begin{code}
 932 unifyTauTyLists :: [TcTauType] -> [TcTauType] ->  TcM ()
 933 unifyTauTyLists []           []         = returnTc ()
 934 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2   `thenTc_`
 935                                         unifyTauTyLists tys1 tys2
 936 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
 937 \end{code}
 938
 939 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
 940 all together.  It is used, for example, when typechecking explicit
 941 lists, when all the elts should be of the same type.
 942
 943 \begin{code}
 944 unifyTauTyList :: [TcTauType] -> TcM ()
 945 unifyTauTyList []                = returnTc ()
 946 unifyTauTyList [ty]              = returnTc ()
 947 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2   `thenTc_`
 948                                    unifyTauTyList tys
 949 \end{code}
 950
 951 %************************************************************************
 952 %*                                                                      *
 953 \subsection[Unify-uTys]{@uTys@: getting down to business}
 954 %*                                                                      *
 955 %************************************************************************
 956
 957 @uTys@ is the heart of the unifier.  Each arg happens twice, because
 958 we want to report errors in terms of synomyms if poss.  The first of
 959 the pair is used in error messages only; it is always the same as the
 960 second, except that if the first is a synonym then the second may be a
 961 de-synonym'd version.  This way we get better error messages.
 962
 963 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
 964
 965 \begin{code}
 966 uTys :: TcTauType -> TcTauType  -- Error reporting ty1 and real ty1
 967                                 -- ty1 is the *expected* type
 968
 969      -> TcTauType -> TcTauType  -- Error reporting ty2 and real ty2
 970                                 -- ty2 is the *actual* type
 971      -> TcM ()
 972
 973         -- Always expand synonyms (see notes at end)
 974         -- (this also throws away FTVs)
 975 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
 976 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
 977
 978         -- Ignore usage annotations inside typechecker
 979 uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
 980 uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
 981
 982         -- Variables; go for uVar
 983 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
 984 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True  tyvar2 ps_ty1 ty1
 985                                         -- "True" means args swapped
 986
 987         -- Predicates
 988 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
 989   | n1 == n2 = uTys t1 t1 t2 t2
 990 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
 991   | c1 == c2 = unifyTauTyLists tys1 tys2
 992 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
 993   | tc1 == tc2 = unifyTauTyLists tys1 tys2
 994
 995         -- Functions; just check the two parts
 996 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
 997   = uTys fun1 fun1 fun2 fun2    `thenTc_`    uTys arg1 arg1 arg2 arg2
 998
 999         -- Type constructors must match
1000 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
1001   | con1 == con2 && length tys1 == length tys2
1002   = unifyTauTyLists tys1 tys2
1003
1004   | con1 == openKindCon
1005         -- When we are doing kind checking, we might match a kind '?'
1006         -- against a kind '*' or '#'.  Notably, CCallable :: ? -> *, and
1007         -- (CCallable Int) and (CCallable Int#) are both OK
1008   = unifyOpenTypeKind ps_ty2
1009
1010         -- Applications need a bit of care!
1011         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
1012         -- NB: we've already dealt with type variables and Notes,
1013         -- so if one type is an App the other one jolly well better be too
1014 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
1015   = case tcSplitAppTy_maybe ty2 of
1016         Just (s2,t2) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
1017         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
1018
1019         -- Now the same, but the other way round
1020         -- Don't swap the types, because the error messages get worse
1021 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
1022   = case tcSplitAppTy_maybe ty1 of
1023         Just (s1,t1) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
1024         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
1025
1026         -- Not expecting for-alls in unification
1027         -- ... but the error message from the unifyMisMatch more informative
1028         -- than a panic message!
1029
1030         -- Anything else fails
1031 uTys ps_ty1 ty1 ps_ty2 ty2  = unifyMisMatch ps_ty1 ps_ty2
1032 \end{code}
1033
1034
1035 Notes on synonyms
1036 ~~~~~~~~~~~~~~~~~
1037 If you are tempted to make a short cut on synonyms, as in this
1038 pseudocode...
1039
1040 \begin{verbatim}
1041 -- NO   uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
1042 -- NO     = if (con1 == con2) then
1043 -- NO   -- Good news!  Same synonym constructors, so we can shortcut
1044 -- NO   -- by unifying their arguments and ignoring their expansions.
1045 -- NO   unifyTauTypeLists args1 args2
1046 -- NO    else
1047 -- NO   -- Never mind.  Just expand them and try again
1048 -- NO   uTys ty1 ty2
1049 \end{verbatim}
1050
1051 then THINK AGAIN.  Here is the whole story, as detected and reported
1052 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
1053 \begin{quotation}
1054 Here's a test program that should detect the problem:
1055
1056 \begin{verbatim}
1057         type Bogus a = Int
1058         x = (1 :: Bogus Char) :: Bogus Bool
1059 \end{verbatim}
1060
1061 The problem with [the attempted shortcut code] is that
1062 \begin{verbatim}
1063         con1 == con2
1064 \end{verbatim}
1065 is not a sufficient condition to be able to use the shortcut!
1066 You also need to know that the type synonym actually USES all
1067 its arguments.  For example, consider the following type synonym
1068 which does not use all its arguments.
1069 \begin{verbatim}
1070         type Bogus a = Int
1071 \end{verbatim}
1072
1073 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
1074 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
1075 would fail, even though the expanded forms (both \tr{Int}) should
1076 match.
1077
1078 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
1079 unnecessarily bind \tr{t} to \tr{Char}.
1080
1081 ... You could explicitly test for the problem synonyms and mark them
1082 somehow as needing expansion, perhaps also issuing a warning to the
1083 user.
1084 \end{quotation}
1085
1086
1087 %************************************************************************
1088 %*                                                                      *
1089 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
1090 %*                                                                      *
1091 %************************************************************************
1092
1093 @uVar@ is called when at least one of the types being unified is a
1094 variable.  It does {\em not} assume that the variable is a fixed point
1095 of the substitution; rather, notice that @uVar@ (defined below) nips
1096 back into @uTys@ if it turns out that the variable is already bound.
1097
1098 \begin{code}
1099 uVar :: Bool            -- False => tyvar is the "expected"
1100                         -- True  => ty    is the "expected" thing
1101      -> TcTyVar
1102      -> TcTauType -> TcTauType  -- printing and real versions
1103      -> TcM ()
1104
1105 uVar swapped tv1 ps_ty2 ty2
1106   = getTcTyVar tv1      `thenNF_Tc` \ maybe_ty1 ->
1107     case maybe_ty1 of
1108         Just ty1 | swapped   -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
1109                  | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
1110         other       -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
1111
1112         -- Expand synonyms; ignore FTVs
1113 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
1114   = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
1115
1116
1117         -- The both-type-variable case
1118 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
1119
1120         -- Same type variable => no-op
1121   | tv1 == tv2
1122   = returnTc ()
1123
1124         -- Distinct type variables
1125         -- ASSERT maybe_ty1 /= Just
1126   | otherwise
1127   = getTcTyVar tv2      `thenNF_Tc` \ maybe_ty2 ->
1128     case maybe_ty2 of
1129         Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
1130
1131         Nothing | update_tv2
1132
1133                 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
1134                    putTcTyVar tv2 (TyVarTy tv1)         `thenNF_Tc_`
1135                    returnTc ()
1136                 |  otherwise
1137
1138                 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
1139                    (putTcTyVar tv1 ps_ty2               `thenNF_Tc_`
1140                     returnTc ())
1141   where
1142     k1 = tyVarKind tv1
1143     k2 = tyVarKind tv2
1144     update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
1145                         -- Try to get rid of open type variables as soon as poss
1146
1147     nicer_to_update_tv2 =  isSigTyVar tv1
1148                                 -- Don't unify a signature type variable if poss
1149                         || isSystemName (varName tv2)
1150                                 -- Try to update sys-y type variables in preference to sig-y ones
1151
1152         -- Second one isn't a type variable
1153 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
1154   =     -- Check that the kinds match
1155     checkKinds swapped tv1 non_var_ty2                  `thenTc_`
1156
1157         -- Check that tv1 isn't a type-signature type variable
1158     checkTcM (not (isSigTyVar tv1))
1159              (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
1160
1161         -- Check that we aren't losing boxity info (shouldn't happen)
1162     warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
1163            ((ppr tv1 <+> ppr (tyVarKind tv1)) $$
1164              (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2)))          `thenNF_Tc_`
1165
1166         -- Occurs check
1167         -- Basically we want to update     tv1 := ps_ty2
1168         -- because ps_ty2 has type-synonym info, which improves later error messages
1169         --
1170         -- But consider
1171         --      type A a = ()
1172         --
1173         --      f :: (A a -> a -> ()) -> ()
1174         --      f = \ _ -> ()
1175         --
1176         --      x :: ()
1177         --      x = f (\ x p -> p x)
1178         --
1179         -- In the application (p x), we try to match "t" with "A t".  If we go
1180         -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
1181         -- an infinite loop later.
1182         -- But we should not reject the program, because A t = ().
1183         -- Rather, we should bind t to () (= non_var_ty2).
1184         --
1185         -- That's why we have this two-state occurs-check
1186     zonkTcType ps_ty2                                   `thenNF_Tc` \ ps_ty2' ->
1187     if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
1188         putTcTyVar tv1 ps_ty2'                          `thenNF_Tc_`
1189         returnTc ()
1190     else
1191     zonkTcType non_var_ty2                              `thenNF_Tc` \ non_var_ty2' ->
1192     if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
1193         -- This branch rarely succeeds, except in strange cases
1194         -- like that in the example above
1195         putTcTyVar tv1 non_var_ty2'                     `thenNF_Tc_`
1196         returnTc ()
1197     else
1198     failWithTcM (unifyOccurCheck tv1 ps_ty2')
1199
1200
1201 checkKinds swapped tv1 ty2
1202 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
1203 -- We need to check that we don't unify a lifted type variable with an
1204 -- unlifted type: e.g.  (id 3#) is illegal
1205   | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
1206   = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)       $
1207     unifyMisMatch k1 k2
1208   | otherwise
1209   = returnTc ()
1210   where
1211     (k1,k2) | swapped   = (tk2,tk1)
1212             | otherwise = (tk1,tk2)
1213     tk1 = tyVarKind tv1
1214     tk2 = typeKind ty2
1215 \end{code}
1216
1217
1218 %************************************************************************
1219 %*                                                                      *
1220 \subsection[Unify-fun]{@unifyFunTy@}
1221 %*                                                                      *
1222 %************************************************************************
1223
1224 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
1225
1226 \begin{code}
1227 unifyFunTy :: TcType                            -- Fail if ty isn't a function type
1228            -> TcM (TcType, TcType)      -- otherwise return arg and result types
1229
1230 unifyFunTy ty@(TyVarTy tyvar)
1231   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
1232     case maybe_ty of
1233         Just ty' -> unifyFunTy ty'
1234         other       -> unify_fun_ty_help ty
1235
1236 unifyFunTy ty
1237   = case tcSplitFunTy_maybe ty of
1238         Just arg_and_res -> returnTc arg_and_res
1239         Nothing          -> unify_fun_ty_help ty
1240
1241 unify_fun_ty_help ty    -- Special cases failed, so revert to ordinary unification
1242   = newTyVarTy openTypeKind     `thenNF_Tc` \ arg ->
1243     newTyVarTy openTypeKind     `thenNF_Tc` \ res ->
1244     unifyTauTy ty (mkFunTy arg res)     `thenTc_`
1245     returnTc (arg,res)
1246 \end{code}
1247
1248 \begin{code}
1249 unifyListTy :: TcType              -- expected list type
1250             -> TcM TcType      -- list element type
1251
1252 unifyListTy ty@(TyVarTy tyvar)
1253   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
1254     case maybe_ty of
1255         Just ty' -> unifyListTy ty'
1256         other    -> unify_list_ty_help ty
1257
1258 unifyListTy ty
1259   = case tcSplitTyConApp_maybe ty of
1260         Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
1261         other                                       -> unify_list_ty_help ty
1262
1263 unify_list_ty_help ty   -- Revert to ordinary unification
1264   = newTyVarTy liftedTypeKind           `thenNF_Tc` \ elt_ty ->
1265     unifyTauTy ty (mkListTy elt_ty)     `thenTc_`
1266     returnTc elt_ty
1267 \end{code}
1268
1269 \begin{code}
1270 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
1271 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
1272   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
1273     case maybe_ty of
1274         Just ty' -> unifyTupleTy boxity arity ty'
1275         other    -> unify_tuple_ty_help boxity arity ty
1276
1277 unifyTupleTy boxity arity ty
1278   = case tcSplitTyConApp_maybe ty of
1279         Just (tycon, arg_tys)
1280                 |  isTupleTyCon tycon
1281                 && tyConArity tycon == arity
1282                 && tupleTyConBoxity tycon == boxity
1283                 -> returnTc arg_tys
1284         other -> unify_tuple_ty_help boxity arity ty
1285
1286 unify_tuple_ty_help boxity arity ty
1287   = newTyVarTys arity kind                              `thenNF_Tc` \ arg_tys ->
1288     unifyTauTy ty (mkTupleTy boxity arity arg_tys)      `thenTc_`
1289     returnTc arg_tys
1290   where
1291     kind | isBoxed boxity = liftedTypeKind
1292          | otherwise      = openTypeKind
1293 \end{code}
1294
1295
1296 %************************************************************************
1297 %*                                                                      *
1298 \subsection[Unify-context]{Errors and contexts}
1299 %*                                                                      *
1300 %************************************************************************
1301
1302 Errors
1303 ~~~~~~
1304
1305 \begin{code}
1306 unifyCtxt s ty1 ty2 tidy_env    -- ty1 expected, ty2 inferred
1307   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
1308     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
1309     returnNF_Tc (err ty1' ty2')
1310   where
1311     err ty1 ty2 = (env1,
1312                    nest 4
1313                         (vcat [
1314                            text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
1315                            text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
1316                         ]))
1317                   where
1318                     (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
1319
1320 unifyKindCtxt swapped tv1 ty2 tidy_env  -- not swapped => tv1 expected, ty2 inferred
1321         -- tv1 is zonked already
1322   = zonkTcType ty2      `thenNF_Tc` \ ty2' ->
1323     returnNF_Tc (err ty2')
1324   where
1325     err ty2 = (env2, ptext SLIT("When matching types") <+>
1326                      sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
1327             where
1328               (pp_expected, pp_actual) | swapped   = (pp2, pp1)
1329                                        | otherwise = (pp1, pp2)
1330               (env1, tv1') = tidyTyVar tidy_env tv1
1331               (env2, ty2') = tidyOpenType  env1 ty2
1332               pp1 = ppr tv1'
1333               pp2 = ppr ty2'
1334
1335 unifyMisMatch ty1 ty2
1336   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
1337     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
1338     let
1339         (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
1340         msg = hang (ptext SLIT("Couldn't match"))
1341                    4 (sep [quotes (ppr tidy_ty1),
1342                            ptext SLIT("against"),
1343                            quotes (ppr tidy_ty2)])
1344     in
1345     failWithTcM (env, msg)
1346
1347 unifyWithSigErr tyvar ty
1348   = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
1349               4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
1350   where
1351     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
1352     (env2, tidy_ty)    = tidyOpenType  env1     ty
1353
1354 unifyOccurCheck tyvar ty
1355   = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
1356               4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
1357   where
1358     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
1359     (env2, tidy_ty)    = tidyOpenType  env1     ty
1360 \end{code}