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