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