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