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