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   -- Unification
  27   unifyTauTy, unifyTauTyList, unifyTauTyLists,
  28   unifyFunTy, unifyListTy, unifyTupleTy,
  29   unifyKind, unifyKinds, unifyOpenTypeKind,
  30
  31   --------------------------------
  32   -- Zonking
  33   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
  34   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
  35   zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
  36
  37   ) where
  38
  39 #include "HsVersions.h"
  40
  41
  42 -- friends:
  43 import TypeRep          ( Type(..), SourceType(..), Kind, TyNote(..),    -- friend
  44                           openKindCon, typeCon
  45                         )
  46 import TcType           ( tcEqType,
  47                           tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe,
  48                           tcSplitTyConApp_maybe, tcSplitFunTy_maybe, tcSplitForAllTys,
  49                           tcGetTyVar, tcIsTyVarTy,
  50
  51                           mkAppTy, mkTyVarTy, mkTyVarTys, mkFunTy, mkTyConApp,
  52
  53                           liftedTypeKind, unliftedTypeKind, openTypeKind, defaultKind, superKind,
  54                           superBoxity, liftedBoxity, hasMoreBoxityInfo, typeKind,
  55                           tyVarsOfType, tyVarsOfTypes, tidyOpenType, tidyOpenTypes, tidyTyVar,
  56                           eqKind,
  57                         )
  58 import Subst            ( Subst, mkTopTyVarSubst, substTy )
  59 import TyCon            ( TyCon, mkPrimTyCon, isTupleTyCon, tyConArity, tupleTyConBoxity )
  60 import PrimRep          ( PrimRep(VoidRep) )
  61 import Var              ( TyVar, varName, tyVarKind, tyVarName, isTyVar, mkTyVar,
  62                           isMutTyVar, isSigTyVar )
  63
  64 -- others:
  65 import TcMonad          -- TcType, amongst others
  66 import TysWiredIn       ( voidTy, listTyCon, mkListTy, mkTupleTy )
  67
  68 import Name             ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
  69                           mkLocalName, mkDerivedTyConOcc, isSystemName
  70                         )
  71 import VarSet
  72 import BasicTypes       ( Boxity, Arity, isBoxed )
  73 import Unique           ( Uniquable(..) )
  74 import SrcLoc           ( noSrcLoc )
  75 import Util             ( nOfThem )
  76 import Outputable
  77 \end{code}
  78
  79
  80 %************************************************************************
  81 %*                                                                      *
  82 \subsection{New type variables}
  83 %*                                                                      *
  84 %************************************************************************
  85
  86 \begin{code}
  87 newTyVar :: Kind -> NF_TcM TcTyVar
  88 newTyVar kind
  89   = tcGetUnique         `thenNF_Tc` \ uniq ->
  90     tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind
  91
  92 newTyVarTy  :: Kind -> NF_TcM TcType
  93 newTyVarTy kind
  94   = newTyVar kind       `thenNF_Tc` \ tc_tyvar ->
  95     returnNF_Tc (TyVarTy tc_tyvar)
  96
  97 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
  98 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
  99
 100 newKindVar :: NF_TcM TcKind
 101 newKindVar
 102   = tcGetUnique                                                 `thenNF_Tc` \ uniq ->
 103     tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind     `thenNF_Tc` \ kv ->
 104     returnNF_Tc (TyVarTy kv)
 105
 106 newKindVars :: Int -> NF_TcM [TcKind]
 107 newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 108
 109 newBoxityVar :: NF_TcM TcKind
 110 newBoxityVar
 111   = tcGetUnique                                                 `thenNF_Tc` \ uniq ->
 112     tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity  `thenNF_Tc` \ kv ->
 113     returnNF_Tc (TyVarTy kv)
 114 \end{code}
 115
 116
 117 %************************************************************************
 118 %*                                                                      *
 119 \subsection{Type instantiation}
 120 %*                                                                      *
 121 %************************************************************************
 122
 123 I don't understand why this is needed
 124 An old comments says "No need for tcSplitForAllTyM because a type
 125         variable can't be instantiated to a for-all type"
 126 But the same is true of rho types!
 127
 128 \begin{code}
 129 tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
 130 tcSplitRhoTyM t
 131   = go t t []
 132  where
 133         -- A type variable is never instantiated to a dictionary type,
 134         -- so we don't need to do a tcReadVar on the "arg".
 135     go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
 136                                         Just pair -> go res res (pair:ts)
 137                                         Nothing   -> returnNF_Tc (reverse ts, syn_t)
 138     go syn_t (NoteTy n t)    ts = go syn_t t ts
 139     go syn_t (TyVarTy tv)    ts = getTcTyVar tv         `thenNF_Tc` \ maybe_ty ->
 140                                   case maybe_ty of
 141                                     Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
 142                                     other                          -> returnNF_Tc (reverse ts, syn_t)
 143     go syn_t (UsageTy _ t)   ts = go syn_t t ts
 144     go syn_t t               ts = returnNF_Tc (reverse ts, syn_t)
 145 \end{code}
 146
 147
 148 %************************************************************************
 149 %*                                                                      *
 150 \subsection{Type instantiation}
 151 %*                                                                      *
 152 %************************************************************************
 153
 154 Instantiating a bunch of type variables
 155
 156 \begin{code}
 157 tcInstTyVars :: [TyVar]
 158              -> NF_TcM ([TcTyVar], [TcType], Subst)
 159
 160 tcInstTyVars tyvars
 161   = mapNF_Tc tcInstTyVar tyvars `thenNF_Tc` \ tc_tyvars ->
 162     let
 163         tys = mkTyVarTys tc_tyvars
 164     in
 165     returnNF_Tc (tc_tyvars, tys, mkTopTyVarSubst tyvars tys)
 166                 -- Since the tyvars are freshly made,
 167                 -- they cannot possibly be captured by
 168                 -- any existing for-alls.  Hence mkTopTyVarSubst
 169
 170 tcInstTyVar tyvar
 171   = tcGetUnique                 `thenNF_Tc` \ uniq ->
 172     let
 173         name = setNameUnique (tyVarName tyvar) uniq
 174         -- Note that we don't change the print-name
 175         -- This won't confuse the type checker but there's a chance
 176         -- that two different tyvars will print the same way
 177         -- in an error message.  -dppr-debug will show up the difference
 178         -- Better watch out for this.  If worst comes to worst, just
 179         -- use mkSysLocalName.
 180     in
 181     tcNewMutTyVar name (tyVarKind tyvar)
 182
 183 tcInstSigVars tyvars    -- Very similar to tcInstTyVar
 184   = tcGetUniques        `thenNF_Tc` \ uniqs ->
 185     listTc [ ASSERT( not (kind `eqKind` openTypeKind) ) -- Shouldn't happen
 186              tcNewSigTyVar name kind
 187            | (tyvar, uniq) <- tyvars `zip` uniqs,
 188              let name = setNameUnique (tyVarName tyvar) uniq,
 189              let kind = tyVarKind tyvar
 190            ]
 191 \end{code}
 192
 193 @tcInstType@ instantiates the outer-level for-alls of a TcType with
 194 fresh type variables, splits off the dictionary part, and returns the results.
 195
 196 \begin{code}
 197 tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
 198 tcInstType ty
 199   = case tcSplitForAllTys ty of
 200         ([],     rho) ->        -- There may be overloading but no type variables;
 201                                 --      (?x :: Int) => Int -> Int
 202                          let
 203                            (theta, tau) = tcSplitRhoTy rho      -- Used to be tcSplitRhoTyM
 204                          in
 205                          returnNF_Tc ([], theta, tau)
 206
 207         (tyvars, rho) -> tcInstTyVars tyvars                    `thenNF_Tc` \ (tyvars', _, tenv)  ->
 208                          let
 209                            (theta, tau) = tcSplitRhoTy (substTy tenv rho)       -- Used to be tcSplitRhoTyM
 210                          in
 211                          returnNF_Tc (tyvars', theta, tau)
 212 \end{code}
 213
 214
 215
 216 %************************************************************************
 217 %*                                                                      *
 218 \subsection{Putting and getting  mutable type variables}
 219 %*                                                                      *
 220 %************************************************************************
 221
 222 \begin{code}
 223 putTcTyVar :: TcTyVar -> TcType -> NF_TcM TcType
 224 getTcTyVar :: TcTyVar -> NF_TcM (Maybe TcType)
 225 \end{code}
 226
 227 Putting is easy:
 228
 229 \begin{code}
 230 putTcTyVar tyvar ty
 231   | not (isMutTyVar tyvar)
 232   = pprTrace "putTcTyVar" (ppr tyvar) $
 233     returnNF_Tc ty
 234
 235   | otherwise
 236   = ASSERT( isMutTyVar tyvar )
 237     UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
 238     tcWriteMutTyVar tyvar (Just ty)     `thenNF_Tc_`
 239     returnNF_Tc ty
 240 \end{code}
 241
 242 Getting is more interesting.  The easy thing to do is just to read, thus:
 243
 244 \begin{verbatim}
 245 getTcTyVar tyvar = tcReadMutTyVar tyvar
 246 \end{verbatim}
 247
 248 But it's more fun to short out indirections on the way: If this
 249 version returns a TyVar, then that TyVar is unbound.  If it returns
 250 any other type, then there might be bound TyVars embedded inside it.
 251
 252 We return Nothing iff the original box was unbound.
 253
 254 \begin{code}
 255 getTcTyVar tyvar
 256   | not (isMutTyVar tyvar)
 257   = pprTrace "getTcTyVar" (ppr tyvar) $
 258     returnNF_Tc (Just (mkTyVarTy tyvar))
 259
 260   | otherwise
 261   = ASSERT2( isMutTyVar tyvar, ppr tyvar )
 262     tcReadMutTyVar tyvar                                `thenNF_Tc` \ maybe_ty ->
 263     case maybe_ty of
 264         Just ty -> short_out ty                         `thenNF_Tc` \ ty' ->
 265                    tcWriteMutTyVar tyvar (Just ty')     `thenNF_Tc_`
 266                    returnNF_Tc (Just ty')
 267
 268         Nothing    -> returnNF_Tc Nothing
 269
 270 short_out :: TcType -> NF_TcM TcType
 271 short_out ty@(TyVarTy tyvar)
 272   | not (isMutTyVar tyvar)
 273   = returnNF_Tc ty
 274
 275   | otherwise
 276   = tcReadMutTyVar tyvar        `thenNF_Tc` \ maybe_ty ->
 277     case maybe_ty of
 278         Just ty' -> short_out ty'                       `thenNF_Tc` \ ty' ->
 279                     tcWriteMutTyVar tyvar (Just ty')    `thenNF_Tc_`
 280                     returnNF_Tc ty'
 281
 282         other    -> returnNF_Tc ty
 283
 284 short_out other_ty = returnNF_Tc other_ty
 285 \end{code}
 286
 287
 288 %************************************************************************
 289 %*                                                                      *
 290 \subsection{Zonking -- the exernal interfaces}
 291 %*                                                                      *
 292 %************************************************************************
 293
 294 -----------------  Type variables
 295
 296 \begin{code}
 297 zonkTcTyVars :: [TcTyVar] -> NF_TcM [TcType]
 298 zonkTcTyVars tyvars = mapNF_Tc zonkTcTyVar tyvars
 299
 300 zonkTcTyVarsAndFV :: [TcTyVar] -> NF_TcM TcTyVarSet
 301 zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars  `thenNF_Tc` \ tys ->
 302                            returnNF_Tc (tyVarsOfTypes tys)
 303
 304 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
 305 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
 306
 307 zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
 308 -- This guy is to zonk the tyvars we're about to feed into tcSimplify
 309 -- Usually this job is done by checkSigTyVars, but in a couple of places
 310 -- that is overkill, so we use this simpler chap
 311 zonkTcSigTyVars tyvars
 312   = zonkTcTyVars tyvars `thenNF_Tc` \ tys ->
 313     returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
 314 \end{code}
 315
 316 -----------------  Types
 317
 318 \begin{code}
 319 zonkTcType :: TcType -> NF_TcM TcType
 320 zonkTcType ty = zonkType (\ tv -> returnNF_Tc (TyVarTy tv)) ty
 321
 322 zonkTcTypes :: [TcType] -> NF_TcM [TcType]
 323 zonkTcTypes tys = mapNF_Tc zonkTcType tys
 324
 325 zonkTcClassConstraints cts = mapNF_Tc zonk cts
 326     where zonk (clas, tys)
 327             = zonkTcTypes tys   `thenNF_Tc` \ new_tys ->
 328               returnNF_Tc (clas, new_tys)
 329
 330 zonkTcThetaType :: TcThetaType -> NF_TcM TcThetaType
 331 zonkTcThetaType theta = mapNF_Tc zonkTcPredType theta
 332
 333 zonkTcPredType :: TcPredType -> NF_TcM TcPredType
 334 zonkTcPredType (ClassP c ts) =
 335     zonkTcTypes ts      `thenNF_Tc` \ new_ts ->
 336     returnNF_Tc (ClassP c new_ts)
 337 zonkTcPredType (IParam n t) =
 338     zonkTcType t        `thenNF_Tc` \ new_t ->
 339     returnNF_Tc (IParam n new_t)
 340 \end{code}
 341
 342 -------------------  These ...ToType, ...ToKind versions
 343                      are used at the end of type checking
 344
 345 \begin{code}
 346 zonkKindEnv :: [(Name, TcKind)] -> NF_TcM [(Name, Kind)]
 347 zonkKindEnv pairs
 348   = mapNF_Tc zonk_it pairs
 349  where
 350     zonk_it (name, tc_kind) = zonkType zonk_unbound_kind_var tc_kind `thenNF_Tc` \ kind ->
 351                               returnNF_Tc (name, kind)
 352
 353         -- When zonking a kind, we want to
 354         --      zonk a *kind* variable to (Type *)
 355         --      zonk a *boxity* variable to *
 356     zonk_unbound_kind_var kv | tyVarKind kv `eqKind` superKind   = putTcTyVar kv liftedTypeKind
 357                              | tyVarKind kv `eqKind` superBoxity = putTcTyVar kv liftedBoxity
 358                              | otherwise                         = pprPanic "zonkKindEnv" (ppr kv)
 359
 360 zonkTcTypeToType :: TcType -> NF_TcM Type
 361 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
 362   where
 363         -- Zonk a mutable but unbound type variable to
 364         --      Void            if it has kind Lifted
 365         --      :Void           otherwise
 366     zonk_unbound_tyvar tv
 367         | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
 368         = putTcTyVar tv voidTy  -- Just to avoid creating a new tycon in
 369                                 -- this vastly common case
 370         | otherwise
 371         = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
 372         where
 373           kind = tyVarKind tv
 374
 375     mk_void_tycon tv kind       -- Make a new TyCon with the same kind as the
 376                                 -- type variable tv.  Same name too, apart from
 377                                 -- making it start with a colon (sigh)
 378                 -- I dread to think what will happen if this gets out into an
 379                 -- interface file.  Catastrophe likely.  Major sigh.
 380         = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
 381           mkPrimTyCon tc_name kind 0 [] VoidRep
 382         where
 383           tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
 384
 385 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence
 386 -- of a type variable, at the *end* of type checking.  It changes
 387 -- the *mutable* type variable into an *immutable* one.
 388 --
 389 -- It does this by making an immutable version of tv and binds tv to it.
 390 -- Now any bound occurences of the original type variable will get
 391 -- zonked to the immutable version.
 392
 393 zonkTcTyVarToTyVar :: TcTyVar -> NF_TcM TyVar
 394 zonkTcTyVarToTyVar tv
 395   = let
 396                 -- Make an immutable version, defaulting
 397                 -- the kind to lifted if necessary
 398         immut_tv    = mkTyVar (tyVarName tv) (defaultKind (tyVarKind tv))
 399         immut_tv_ty = mkTyVarTy immut_tv
 400
 401         zap tv = putTcTyVar tv immut_tv_ty
 402                 -- Bind the mutable version to the immutable one
 403     in
 404         -- If the type variable is mutable, then bind it to immut_tv_ty
 405         -- so that all other occurrences of the tyvar will get zapped too
 406     zonkTyVar zap tv            `thenNF_Tc` \ ty2 ->
 407
 408     WARN( not (immut_tv_ty `tcEqType` ty2), ppr tv $$ ppr immut_tv $$ ppr ty2 )
 409
 410     returnNF_Tc immut_tv
 411 \end{code}
 412
 413
 414 %************************************************************************
 415 %*                                                                      *
 416 \subsection{Zonking -- the main work-horses: zonkType, zonkTyVar}
 417 %*                                                                      *
 418 %*              For internal use only!                                  *
 419 %*                                                                      *
 420 %************************************************************************
 421
 422 \begin{code}
 423 -- zonkType is used for Kinds as well
 424
 425 -- For unbound, mutable tyvars, zonkType uses the function given to it
 426 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 427 --      type variable and zonks the kind too
 428
 429 zonkType :: (TcTyVar -> NF_TcM Type)    -- What to do with unbound mutable type variables
 430                                         -- see zonkTcType, and zonkTcTypeToType
 431          -> TcType
 432          -> NF_TcM Type
 433 zonkType unbound_var_fn ty
 434   = go ty
 435   where
 436     go (TyConApp tycon tys)       = mapNF_Tc go tys     `thenNF_Tc` \ tys' ->
 437                                     returnNF_Tc (TyConApp tycon tys')
 438
 439     go (NoteTy (SynNote ty1) ty2) = go ty1              `thenNF_Tc` \ ty1' ->
 440                                     go ty2              `thenNF_Tc` \ ty2' ->
 441                                     returnNF_Tc (NoteTy (SynNote ty1') ty2')
 442
 443     go (NoteTy (FTVNote _) ty2)   = go ty2      -- Discard free-tyvar annotations
 444
 445     go (SourceTy p)               = go_pred p           `thenNF_Tc` \ p' ->
 446                                     returnNF_Tc (SourceTy p')
 447
 448     go (FunTy arg res)            = go arg              `thenNF_Tc` \ arg' ->
 449                                     go res              `thenNF_Tc` \ res' ->
 450                                     returnNF_Tc (FunTy arg' res')
 451
 452     go (AppTy fun arg)            = go fun              `thenNF_Tc` \ fun' ->
 453                                     go arg              `thenNF_Tc` \ arg' ->
 454                                     returnNF_Tc (mkAppTy fun' arg')
 455
 456     go (UsageTy u ty)             = go u                `thenNF_Tc` \ u'  ->
 457                                     go ty               `thenNF_Tc` \ ty' ->
 458                                     returnNF_Tc (UsageTy u' ty')
 459
 460         -- The two interesting cases!
 461     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
 462
 463     go (ForAllTy tyvar ty) = zonkTcTyVarToTyVar tyvar   `thenNF_Tc` \ tyvar' ->
 464                              go ty                      `thenNF_Tc` \ ty' ->
 465                              returnNF_Tc (ForAllTy tyvar' ty')
 466
 467     go_pred (ClassP c tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
 468                              returnNF_Tc (ClassP c tys')
 469     go_pred (NType tc tys) = mapNF_Tc go tys    `thenNF_Tc` \ tys' ->
 470                              returnNF_Tc (NType tc tys')
 471     go_pred (IParam n ty) = go ty               `thenNF_Tc` \ ty' ->
 472                             returnNF_Tc (IParam n ty')
 473
 474 zonkTyVar :: (TcTyVar -> NF_TcM Type)           -- What to do for an unbound mutable variable
 475           -> TcTyVar -> NF_TcM TcType
 476 zonkTyVar unbound_var_fn tyvar
 477   | not (isMutTyVar tyvar)      -- Not a mutable tyvar.  This can happen when
 478                                 -- zonking a forall type, when the bound type variable
 479                                 -- needn't be mutable
 480   = ASSERT( isTyVar tyvar )             -- Should not be any immutable kind vars
 481     returnNF_Tc (TyVarTy tyvar)
 482
 483   | otherwise
 484   =  getTcTyVar tyvar   `thenNF_Tc` \ maybe_ty ->
 485      case maybe_ty of
 486           Nothing       -> unbound_var_fn tyvar                 -- Mutable and unbound
 487           Just other_ty -> zonkType unbound_var_fn other_ty     -- Bound
 488 \end{code}
 489
 490
 491
 492 %************************************************************************
 493 %*                                                                      *
 494 \subsection{The Kind variants}
 495 %*                                                                      *
 496 %************************************************************************
 497
 498 \begin{code}
 499 unifyKind :: TcKind                 -- Expected
 500           -> TcKind                 -- Actual
 501           -> TcM ()
 502 unifyKind k1 k2
 503   = tcAddErrCtxtM (unifyCtxt "kind" k1 k2) $
 504     uTys k1 k1 k2 k2
 505
 506 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
 507 unifyKinds []       []       = returnTc ()
 508 unifyKinds (k1:ks1) (k2:ks2) = unifyKind k1 k2  `thenTc_`
 509                                unifyKinds ks1 ks2
 510 unifyKinds _ _ = panic "unifyKinds: length mis-match"
 511 \end{code}
 512
 513 \begin{code}
 514 unifyOpenTypeKind :: TcKind -> TcM ()
 515 -- Ensures that the argument kind is of the form (Type bx)
 516 -- for some boxity bx
 517
 518 unifyOpenTypeKind ty@(TyVarTy tyvar)
 519   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 520     case maybe_ty of
 521         Just ty' -> unifyOpenTypeKind ty'
 522         other    -> unify_open_kind_help ty
 523
 524 unifyOpenTypeKind ty
 525   = case tcSplitTyConApp_maybe ty of
 526         Just (tycon, [_]) | tycon == typeCon -> returnTc ()
 527         other                                -> unify_open_kind_help ty
 528
 529 unify_open_kind_help ty -- Revert to ordinary unification
 530   = newBoxityVar        `thenNF_Tc` \ boxity ->
 531     unifyKind ty (mkTyConApp typeCon [boxity])
 532 \end{code}
 533
 534
 535 %************************************************************************
 536 %*                                                                      *
 537 \subsection[Unify-exported]{Exported unification functions}
 538 %*                                                                      *
 539 %************************************************************************
 540
 541 The exported functions are all defined as versions of some
 542 non-exported generic functions.
 543
 544 Unify two @TauType@s.  Dead straightforward.
 545
 546 \begin{code}
 547 unifyTauTy :: TcTauType -> TcTauType -> TcM ()
 548 unifyTauTy ty1 ty2      -- ty1 expected, ty2 inferred
 549   = tcAddErrCtxtM (unifyCtxt "type" ty1 ty2) $
 550     uTys ty1 ty1 ty2 ty2
 551 \end{code}
 552
 553 @unifyTauTyList@ unifies corresponding elements of two lists of
 554 @TauType@s.  It uses @uTys@ to do the real work.  The lists should be
 555 of equal length.  We charge down the list explicitly so that we can
 556 complain if their lengths differ.
 557
 558 \begin{code}
 559 unifyTauTyLists :: [TcTauType] -> [TcTauType] ->  TcM ()
 560 unifyTauTyLists []           []         = returnTc ()
 561 unifyTauTyLists (ty1:tys1) (ty2:tys2) = uTys ty1 ty1 ty2 ty2   `thenTc_`
 562                                         unifyTauTyLists tys1 tys2
 563 unifyTauTyLists ty1s ty2s = panic "Unify.unifyTauTyLists: mismatched type lists!"
 564 \end{code}
 565
 566 @unifyTauTyList@ takes a single list of @TauType@s and unifies them
 567 all together.  It is used, for example, when typechecking explicit
 568 lists, when all the elts should be of the same type.
 569
 570 \begin{code}
 571 unifyTauTyList :: [TcTauType] -> TcM ()
 572 unifyTauTyList []                = returnTc ()
 573 unifyTauTyList [ty]              = returnTc ()
 574 unifyTauTyList (ty1:tys@(ty2:_)) = unifyTauTy ty1 ty2   `thenTc_`
 575                                    unifyTauTyList tys
 576 \end{code}
 577
 578 %************************************************************************
 579 %*                                                                      *
 580 \subsection[Unify-uTys]{@uTys@: getting down to business}
 581 %*                                                                      *
 582 %************************************************************************
 583
 584 @uTys@ is the heart of the unifier.  Each arg happens twice, because
 585 we want to report errors in terms of synomyms if poss.  The first of
 586 the pair is used in error messages only; it is always the same as the
 587 second, except that if the first is a synonym then the second may be a
 588 de-synonym'd version.  This way we get better error messages.
 589
 590 We call the first one \tr{ps_ty1}, \tr{ps_ty2} for ``possible synomym''.
 591
 592 \begin{code}
 593 uTys :: TcTauType -> TcTauType  -- Error reporting ty1 and real ty1
 594                                 -- ty1 is the *expected* type
 595
 596      -> TcTauType -> TcTauType  -- Error reporting ty2 and real ty2
 597                                 -- ty2 is the *actual* type
 598      -> TcM ()
 599
 600         -- Always expand synonyms (see notes at end)
 601         -- (this also throws away FTVs)
 602 uTys ps_ty1 (NoteTy n1 ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
 603 uTys ps_ty1 ty1 ps_ty2 (NoteTy n2 ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
 604
 605         -- Ignore usage annotations inside typechecker
 606 uTys ps_ty1 (UsageTy _ ty1) ps_ty2 ty2 = uTys ps_ty1 ty1 ps_ty2 ty2
 607 uTys ps_ty1 ty1 ps_ty2 (UsageTy _ ty2) = uTys ps_ty1 ty1 ps_ty2 ty2
 608
 609         -- Variables; go for uVar
 610 uTys ps_ty1 (TyVarTy tyvar1) ps_ty2 ty2 = uVar False tyvar1 ps_ty2 ty2
 611 uTys ps_ty1 ty1 ps_ty2 (TyVarTy tyvar2) = uVar True  tyvar2 ps_ty1 ty1
 612                                         -- "True" means args swapped
 613
 614         -- Predicates
 615 uTys _ (SourceTy (IParam n1 t1)) _ (SourceTy (IParam n2 t2))
 616   | n1 == n2 = uTys t1 t1 t2 t2
 617 uTys _ (SourceTy (ClassP c1 tys1)) _ (SourceTy (ClassP c2 tys2))
 618   | c1 == c2 = unifyTauTyLists tys1 tys2
 619 uTys _ (SourceTy (NType tc1 tys1)) _ (SourceTy (NType tc2 tys2))
 620   | tc1 == tc2 = unifyTauTyLists tys1 tys2
 621
 622         -- Functions; just check the two parts
 623 uTys _ (FunTy fun1 arg1) _ (FunTy fun2 arg2)
 624   = uTys fun1 fun1 fun2 fun2    `thenTc_`    uTys arg1 arg1 arg2 arg2
 625
 626         -- Type constructors must match
 627 uTys ps_ty1 (TyConApp con1 tys1) ps_ty2 (TyConApp con2 tys2)
 628   | con1 == con2 && length tys1 == length tys2
 629   = unifyTauTyLists tys1 tys2
 630
 631   | con1 == openKindCon
 632         -- When we are doing kind checking, we might match a kind '?'
 633         -- against a kind '*' or '#'.  Notably, CCallable :: ? -> *, and
 634         -- (CCallable Int) and (CCallable Int#) are both OK
 635   = unifyOpenTypeKind ps_ty2
 636
 637         -- Applications need a bit of care!
 638         -- They can match FunTy and TyConApp, so use splitAppTy_maybe
 639         -- NB: we've already dealt with type variables and Notes,
 640         -- so if one type is an App the other one jolly well better be too
 641 uTys ps_ty1 (AppTy s1 t1) ps_ty2 ty2
 642   = case tcSplitAppTy_maybe ty2 of
 643         Just (s2,t2) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
 644         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 645
 646         -- Now the same, but the other way round
 647         -- Don't swap the types, because the error messages get worse
 648 uTys ps_ty1 ty1 ps_ty2 (AppTy s2 t2)
 649   = case tcSplitAppTy_maybe ty1 of
 650         Just (s1,t1) -> uTys s1 s1 s2 s2        `thenTc_`    uTys t1 t1 t2 t2
 651         Nothing      -> unifyMisMatch ps_ty1 ps_ty2
 652
 653         -- Not expecting for-alls in unification
 654         -- ... but the error message from the unifyMisMatch more informative
 655         -- than a panic message!
 656
 657         -- Anything else fails
 658 uTys ps_ty1 ty1 ps_ty2 ty2  = unifyMisMatch ps_ty1 ps_ty2
 659 \end{code}
 660
 661
 662 Notes on synonyms
 663 ~~~~~~~~~~~~~~~~~
 664 If you are tempted to make a short cut on synonyms, as in this
 665 pseudocode...
 666
 667 \begin{verbatim}
 668 -- NO   uTys (SynTy con1 args1 ty1) (SynTy con2 args2 ty2)
 669 -- NO     = if (con1 == con2) then
 670 -- NO   -- Good news!  Same synonym constructors, so we can shortcut
 671 -- NO   -- by unifying their arguments and ignoring their expansions.
 672 -- NO   unifyTauTypeLists args1 args2
 673 -- NO    else
 674 -- NO   -- Never mind.  Just expand them and try again
 675 -- NO   uTys ty1 ty2
 676 \end{verbatim}
 677
 678 then THINK AGAIN.  Here is the whole story, as detected and reported
 679 by Chris Okasaki \tr{<Chris_Okasaki@loch.mess.cs.cmu.edu>}:
 680 \begin{quotation}
 681 Here's a test program that should detect the problem:
 682
 683 \begin{verbatim}
 684         type Bogus a = Int
 685         x = (1 :: Bogus Char) :: Bogus Bool
 686 \end{verbatim}
 687
 688 The problem with [the attempted shortcut code] is that
 689 \begin{verbatim}
 690         con1 == con2
 691 \end{verbatim}
 692 is not a sufficient condition to be able to use the shortcut!
 693 You also need to know that the type synonym actually USES all
 694 its arguments.  For example, consider the following type synonym
 695 which does not use all its arguments.
 696 \begin{verbatim}
 697         type Bogus a = Int
 698 \end{verbatim}
 699
 700 If you ever tried unifying, say, \tr{Bogus Char} with \tr{Bogus Bool},
 701 the unifier would blithely try to unify \tr{Char} with \tr{Bool} and
 702 would fail, even though the expanded forms (both \tr{Int}) should
 703 match.
 704
 705 Similarly, unifying \tr{Bogus Char} with \tr{Bogus t} would
 706 unnecessarily bind \tr{t} to \tr{Char}.
 707
 708 ... You could explicitly test for the problem synonyms and mark them
 709 somehow as needing expansion, perhaps also issuing a warning to the
 710 user.
 711 \end{quotation}
 712
 713
 714 %************************************************************************
 715 %*                                                                      *
 716 \subsection[Unify-uVar]{@uVar@: unifying with a type variable}
 717 %*                                                                      *
 718 %************************************************************************
 719
 720 @uVar@ is called when at least one of the types being unified is a
 721 variable.  It does {\em not} assume that the variable is a fixed point
 722 of the substitution; rather, notice that @uVar@ (defined below) nips
 723 back into @uTys@ if it turns out that the variable is already bound.
 724
 725 \begin{code}
 726 uVar :: Bool            -- False => tyvar is the "expected"
 727                         -- True  => ty    is the "expected" thing
 728      -> TcTyVar
 729      -> TcTauType -> TcTauType  -- printing and real versions
 730      -> TcM ()
 731
 732 uVar swapped tv1 ps_ty2 ty2
 733   = getTcTyVar tv1      `thenNF_Tc` \ maybe_ty1 ->
 734     case maybe_ty1 of
 735         Just ty1 | swapped   -> uTys ps_ty2 ty2 ty1 ty1 -- Swap back
 736                  | otherwise -> uTys ty1 ty1 ps_ty2 ty2 -- Same order
 737         other       -> uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 738
 739         -- Expand synonyms; ignore FTVs
 740 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 (NoteTy n2 ty2)
 741   = uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2
 742
 743
 744         -- The both-type-variable case
 745 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 ty2@(TyVarTy tv2)
 746
 747         -- Same type variable => no-op
 748   | tv1 == tv2
 749   = returnTc ()
 750
 751         -- Distinct type variables
 752         -- ASSERT maybe_ty1 /= Just
 753   | otherwise
 754   = getTcTyVar tv2      `thenNF_Tc` \ maybe_ty2 ->
 755     case maybe_ty2 of
 756         Just ty2' -> uUnboundVar swapped tv1 maybe_ty1 ty2' ty2'
 757
 758         Nothing | update_tv2
 759
 760                 -> WARN( not (k1 `hasMoreBoxityInfo` k2), (ppr tv1 <+> ppr k1) $$ (ppr tv2 <+> ppr k2) )
 761                    putTcTyVar tv2 (TyVarTy tv1)         `thenNF_Tc_`
 762                    returnTc ()
 763                 |  otherwise
 764
 765                 -> WARN( not (k2 `hasMoreBoxityInfo` k1), (ppr tv2 <+> ppr k2) $$ (ppr tv1 <+> ppr k1) )
 766                    (putTcTyVar tv1 ps_ty2               `thenNF_Tc_`
 767                     returnTc ())
 768   where
 769     k1 = tyVarKind tv1
 770     k2 = tyVarKind tv2
 771     update_tv2 = (k2 `eqKind` openTypeKind) || (not (k1 `eqKind` openTypeKind) && nicer_to_update_tv2)
 772                         -- Try to get rid of open type variables as soon as poss
 773
 774     nicer_to_update_tv2 =  isSigTyVar tv1
 775                                 -- Don't unify a signature type variable if poss
 776                         || isSystemName (varName tv2)
 777                                 -- Try to update sys-y type variables in preference to sig-y ones
 778
 779         -- Second one isn't a type variable
 780 uUnboundVar swapped tv1 maybe_ty1 ps_ty2 non_var_ty2
 781   =     -- Check that the kinds match
 782     checkKinds swapped tv1 non_var_ty2                  `thenTc_`
 783
 784         -- Check that tv1 isn't a type-signature type variable
 785     checkTcM (not (isSigTyVar tv1))
 786              (failWithTcM (unifyWithSigErr tv1 ps_ty2)) `thenTc_`
 787
 788         -- Check that we aren't losing boxity info (shouldn't happen)
 789     warnTc (not (typeKind non_var_ty2 `hasMoreBoxityInfo` tyVarKind tv1))
 790            ((ppr tv1 <+> ppr (tyVarKind tv1)) $$
 791              (ppr non_var_ty2 <+> ppr (typeKind non_var_ty2)))          `thenNF_Tc_`
 792
 793         -- Occurs check
 794         -- Basically we want to update     tv1 := ps_ty2
 795         -- because ps_ty2 has type-synonym info, which improves later error messages
 796         --
 797         -- But consider
 798         --      type A a = ()
 799         --
 800         --      f :: (A a -> a -> ()) -> ()
 801         --      f = \ _ -> ()
 802         --
 803         --      x :: ()
 804         --      x = f (\ x p -> p x)
 805         --
 806         -- In the application (p x), we try to match "t" with "A t".  If we go
 807         -- ahead and bind t to A t (= ps_ty2), we'll lead the type checker into
 808         -- an infinite loop later.
 809         -- But we should not reject the program, because A t = ().
 810         -- Rather, we should bind t to () (= non_var_ty2).
 811         --
 812         -- That's why we have this two-state occurs-check
 813     zonkTcType ps_ty2                                   `thenNF_Tc` \ ps_ty2' ->
 814     if not (tv1 `elemVarSet` tyVarsOfType ps_ty2') then
 815         putTcTyVar tv1 ps_ty2'                          `thenNF_Tc_`
 816         returnTc ()
 817     else
 818     zonkTcType non_var_ty2                              `thenNF_Tc` \ non_var_ty2' ->
 819     if not (tv1 `elemVarSet` tyVarsOfType non_var_ty2') then
 820         -- This branch rarely succeeds, except in strange cases
 821         -- like that in the example above
 822         putTcTyVar tv1 non_var_ty2'                     `thenNF_Tc_`
 823         returnTc ()
 824     else
 825     failWithTcM (unifyOccurCheck tv1 ps_ty2')
 826
 827
 828 checkKinds swapped tv1 ty2
 829 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
 830 -- We need to check that we don't unify a lifted type variable with an
 831 -- unlifted type: e.g.  (id 3#) is illegal
 832   | tk1 `eqKind` liftedTypeKind && tk2 `eqKind` unliftedTypeKind
 833   = tcAddErrCtxtM (unifyKindCtxt swapped tv1 ty2)       $
 834     unifyMisMatch k1 k2
 835   | otherwise
 836   = returnTc ()
 837   where
 838     (k1,k2) | swapped   = (tk2,tk1)
 839             | otherwise = (tk1,tk2)
 840     tk1 = tyVarKind tv1
 841     tk2 = typeKind ty2
 842 \end{code}
 843
 844
 845 %************************************************************************
 846 %*                                                                      *
 847 \subsection[Unify-fun]{@unifyFunTy@}
 848 %*                                                                      *
 849 %************************************************************************
 850
 851 @unifyFunTy@ is used to avoid the fruitless creation of type variables.
 852
 853 \begin{code}
 854 unifyFunTy :: TcType                            -- Fail if ty isn't a function type
 855            -> TcM (TcType, TcType)      -- otherwise return arg and result types
 856
 857 unifyFunTy ty@(TyVarTy tyvar)
 858   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 859     case maybe_ty of
 860         Just ty' -> unifyFunTy ty'
 861         other       -> unify_fun_ty_help ty
 862
 863 unifyFunTy ty
 864   = case tcSplitFunTy_maybe ty of
 865         Just arg_and_res -> returnTc arg_and_res
 866         Nothing          -> unify_fun_ty_help ty
 867
 868 unify_fun_ty_help ty    -- Special cases failed, so revert to ordinary unification
 869   = newTyVarTy openTypeKind     `thenNF_Tc` \ arg ->
 870     newTyVarTy openTypeKind     `thenNF_Tc` \ res ->
 871     unifyTauTy ty (mkFunTy arg res)     `thenTc_`
 872     returnTc (arg,res)
 873 \end{code}
 874
 875 \begin{code}
 876 unifyListTy :: TcType              -- expected list type
 877             -> TcM TcType      -- list element type
 878
 879 unifyListTy ty@(TyVarTy tyvar)
 880   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 881     case maybe_ty of
 882         Just ty' -> unifyListTy ty'
 883         other    -> unify_list_ty_help ty
 884
 885 unifyListTy ty
 886   = case tcSplitTyConApp_maybe ty of
 887         Just (tycon, [arg_ty]) | tycon == listTyCon -> returnTc arg_ty
 888         other                                       -> unify_list_ty_help ty
 889
 890 unify_list_ty_help ty   -- Revert to ordinary unification
 891   = newTyVarTy liftedTypeKind           `thenNF_Tc` \ elt_ty ->
 892     unifyTauTy ty (mkListTy elt_ty)     `thenTc_`
 893     returnTc elt_ty
 894 \end{code}
 895
 896 \begin{code}
 897 unifyTupleTy :: Boxity -> Arity -> TcType -> TcM [TcType]
 898 unifyTupleTy boxity arity ty@(TyVarTy tyvar)
 899   = getTcTyVar tyvar    `thenNF_Tc` \ maybe_ty ->
 900     case maybe_ty of
 901         Just ty' -> unifyTupleTy boxity arity ty'
 902         other    -> unify_tuple_ty_help boxity arity ty
 903
 904 unifyTupleTy boxity arity ty
 905   = case tcSplitTyConApp_maybe ty of
 906         Just (tycon, arg_tys)
 907                 |  isTupleTyCon tycon
 908                 && tyConArity tycon == arity
 909                 && tupleTyConBoxity tycon == boxity
 910                 -> returnTc arg_tys
 911         other -> unify_tuple_ty_help boxity arity ty
 912
 913 unify_tuple_ty_help boxity arity ty
 914   = newTyVarTys arity kind                              `thenNF_Tc` \ arg_tys ->
 915     unifyTauTy ty (mkTupleTy boxity arity arg_tys)      `thenTc_`
 916     returnTc arg_tys
 917   where
 918     kind | isBoxed boxity = liftedTypeKind
 919          | otherwise      = openTypeKind
 920 \end{code}
 921
 922
 923 %************************************************************************
 924 %*                                                                      *
 925 \subsection[Unify-context]{Errors and contexts}
 926 %*                                                                      *
 927 %************************************************************************
 928
 929 Errors
 930 ~~~~~~
 931
 932 \begin{code}
 933 unifyCtxt s ty1 ty2 tidy_env    -- ty1 expected, ty2 inferred
 934   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 935     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 936     returnNF_Tc (err ty1' ty2')
 937   where
 938     err ty1 ty2 = (env1,
 939                    nest 4
 940                         (vcat [
 941                            text "Expected" <+> text s <> colon <+> ppr tidy_ty1,
 942                            text "Inferred" <+> text s <> colon <+> ppr tidy_ty2
 943                         ]))
 944                   where
 945                     (env1, [tidy_ty1,tidy_ty2]) = tidyOpenTypes tidy_env [ty1,ty2]
 946
 947 unifyKindCtxt swapped tv1 ty2 tidy_env  -- not swapped => tv1 expected, ty2 inferred
 948         -- tv1 is zonked already
 949   = zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 950     returnNF_Tc (err ty2')
 951   where
 952     err ty2 = (env2, ptext SLIT("When matching types") <+>
 953                      sep [quotes pp_expected, ptext SLIT("and"), quotes pp_actual])
 954             where
 955               (pp_expected, pp_actual) | swapped   = (pp2, pp1)
 956                                        | otherwise = (pp1, pp2)
 957               (env1, tv1') = tidyTyVar tidy_env tv1
 958               (env2, ty2') = tidyOpenType  env1 ty2
 959               pp1 = ppr tv1'
 960               pp2 = ppr ty2'
 961
 962 unifyMisMatch ty1 ty2
 963   = zonkTcType ty1      `thenNF_Tc` \ ty1' ->
 964     zonkTcType ty2      `thenNF_Tc` \ ty2' ->
 965     let
 966         (env, [tidy_ty1, tidy_ty2]) = tidyOpenTypes emptyTidyEnv [ty1',ty2']
 967         msg = hang (ptext SLIT("Couldn't match"))
 968                    4 (sep [quotes (ppr tidy_ty1),
 969                            ptext SLIT("against"),
 970                            quotes (ppr tidy_ty2)])
 971     in
 972     failWithTcM (env, msg)
 973
 974 unifyWithSigErr tyvar ty
 975   = (env2, hang (ptext SLIT("Cannot unify the type-signature variable") <+> quotes (ppr tidy_tyvar))
 976               4 (ptext SLIT("with the type") <+> quotes (ppr tidy_ty)))
 977   where
 978     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
 979     (env2, tidy_ty)    = tidyOpenType  env1     ty
 980
 981 unifyOccurCheck tyvar ty
 982   = (env2, hang (ptext SLIT("Occurs check: cannot construct the infinite type:"))
 983               4 (sep [ppr tidy_tyvar, char '=', ppr tidy_ty]))
 984   where
 985     (env1, tidy_tyvar) = tidyTyVar emptyTidyEnv tyvar
 986     (env2, tidy_ty)    = tidyOpenType  env1     ty
 987 \end{code}