ghc/compiler/typecheck/Subst.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1995
   3 %
   4 \section[Subst]{Substitutions}
   5
   6 \begin{code}
   7 #include "HsVersions.h"
   8
   9 module Subst (
  10         Subst, SubstResult(..), -- Subst is an abstract data type
  11
  12         mkEmptySubst, extendSubst,
  13
  14 --not exported: applySubstToTauTy,
  15         applySubstToTy,
  16         applySubstToThetaTy, applySubstToTyVar,
  17
  18         getSubstTyVarUniques, getSubstTyVarUnique,
  19
  20         pushSubstUndos, combineSubstUndos, undoSubstUndos,
  21         -- pruneSubst,
  22
  23         -- and to make the interface self-sufficient...
  24         TyVar, UniType
  25     ) where
  26
  27 import AbsUniType       -- lots of stuff, plus...
  28 import UniType          -- UniType(..) -- *********** YOW!!! ********
  29 import Bag              ( emptyBag, unionBags, snocBag,
  30                           bagToList, filterBag, unitBag, Bag )
  31 import Maybes           ( Maybe(..), maybeToBool )
  32 import Outputable
  33 import Unique
  34 import Util
  35 \end{code}
  36
  37 %************************************************************************
  38 %*                                                                      *
  39 \subsection[Subst-magic-importst]{Funny imports to support magic implementation}
  40 %*                                                                      *
  41 %************************************************************************
  42
  43 Or lack thereof.
  44
  45 If we are compiling with Glasgow Haskell we can use mutable
  46 arrays to implement the substitution ...
  47
  48 \begin{code}
  49 #ifndef __GLASGOW_HASKELL__
  50
  51 import LiftMonad
  52
  53 #else {- __GLASGOW_HASKELL__ -}
  54
  55 import PreludeGlaST
  56
  57 type STWorld = _State _RealWorld
  58
  59 newWorld (S# real_world) = S# real_world
  60
  61 #endif {- __GLASGOW_HASKELL__ -}
  62 \end{code}
  63
  64 %************************************************************************
  65 %*                                                                      *
  66 \subsection[Subst-common]{@Subst@: common implementation-independent bits}
  67 %*                                                                      *
  68 %************************************************************************
  69
  70 \begin{code}
  71 data SubstResult
  72   = SubstOK
  73   | OccursCheck     TyVar
  74                     TauType
  75   | AlreadyBound    TauType -- The variable is already bound
  76                             -- to this type.  The type is *not*
  77                             -- necessarily a fixed pt of the
  78                             -- substitution
  79 \end{code}
  80
  81 Common signatures of major functions.
  82
  83 \begin{code}
  84 mkEmptySubst :: Int -> Subst
  85 \end{code}
  86
  87 %---------
  88
  89 @extendSubst@: Add a single binding to the substitution. We have to:
  90 \begin{itemize}
  91 \item
  92 apply the existing bindings to the new one;
  93 \item
  94 check whether we are adding a trivial substitution of a type
  95 variable to itself (if so, do nothing);
  96 \item
  97 perform an occurs check on the right-hand side of the new binding;
  98 \end{itemize}
  99 We do not apply the new binding to all the existing ones. This is
 100 delayed until the substitution is applied.
 101 \begin{code}
 102 extendSubst :: TyVar            -- Tyvar to bind
 103             -> TauType          -- Type to bind it to; NB can be a synonym
 104             -> SubstM SubstResult
 105 \end{code}
 106
 107 %---------
 108
 109 Apply a substitution to a given type.
 110
 111         {\em The type returned is guaranteed to be
 112         a fixed point of the substitution.}
 113
 114 Hence, we have to traverse the type determining the type mapped to
 115 tyvars. The type mapped must be recusively traversed as the substition
 116 is not stored idempotently.
 117
 118 @applySubstToTauTy@ does not expect to meet a dict or forall type.
 119 @applySubstToTy@ may encounter these, but complains if the forall
 120 binds a variable which is in the domain of the substitution.
 121
 122 \begin{code}
 123 applySubstToTy      :: Subst -> UniType   -> (Subst, UniType)
 124 applySubstToTauTy   :: Subst -> TauType   -> (Subst, TauType)
 125 applySubstToThetaTy :: Subst -> ThetaType -> (Subst, ThetaType)
 126 applySubstToTyVar   :: Subst -> TyVar     -> (Subst, TauType)
 127 \end{code}
 128
 129 These functions are only used by the type checker.  We know that
 130 all the for-all'd type variables are fixed points of the substitution,
 131 so it's quite safe just to apply the substitution inside foralls.
 132
 133 %---------
 134
 135 Sorta obvious.
 136 \begin{code}
 137 getSubstTyVarUnique  :: Subst -> (Subst, Unique)
 138 getSubstTyVarUniques :: Int -> Subst -> (Subst, [Unique])
 139 \end{code}
 140
 141 %---------
 142
 143 @pushSubstUndos@ starts a new subst undo scope, saving the old scopes.
 144 It also saves the current unique supply so that it can be restored if
 145 the typecheck fails.
 146
 147 @combineSubstUndos@ is called after a successful typecheck. It
 148 combines the current undos with the previos ones in case we fail in an
 149 outer scope. If no previous undos exist the undos are thrown away as
 150 we must have succeeded at the top level. The unique supply of the
 151 successful scope is returned to the unique supply of the current
 152 scope.
 153
 154 @undoSubstUndos@ is called when a typecheck failed. The any
 155 substitution modifications are undone and the undo information
 156 discarded. The saved unique supply of the enclosing scope is restored.
 157 \begin{code}
 158 pushSubstUndos, combineSubstUndos, undoSubstUndos :: Subst -> Subst
 159 \end{code}
 160
 161 %************************************************************************
 162 %*                                                                      *
 163 \subsection[Subst-Arrays]{@Subst@ with mutable @Arrays@ !!!}
 164 %*                                                                      *
 165 %************************************************************************
 166
 167 Depends on....
 168 \begin{code}
 169 #ifdef __GLASGOW_HASKELL__
 170 \end{code}
 171
 172 %************************************************************************
 173 %*                                                                      *
 174 \subsubsection{@Subst@: specification and representation}
 175 %*                                                                      *
 176 %************************************************************************
 177
 178 {\em Specification:}
 179 * When new bindings are added to the substitution, an occurs check is performed.
 180 * The applySubst function guarantees to return a fixed point of the substitution.
 181
 182 {\em Representation:}
 183 A substitution binds type variables to tau-types, that is @UniType@s without
 184 any @UniForall@ or @UniDict@ constructors.
 185
 186 It is represented as an array, indexed on Int, with a world
 187 token, and a stack of type variables whos subst may be undone. The
 188 array is extended (by copying) if it overflows. The supply of
 189 Ints and the size of the array are linked so the substitution
 190 is also responsible for allocating the supply of uniques.
 191
 192 The undo information is a stack of bags of the nested modifications to
 193 the substitution. If the typecheck fails the modifications to the
 194 substition are undone. If it succeeds the current undos are combined
 195 with the undos in the enclosing scope so that they would be undone if
 196 the enclsing scope typecheck fails.
 197
 198 The unique supply is also stacked so that it can be restored if a
 199 typecheck fails.
 200
 201 NOTE: The uniqueness of the world token, and hence the substitution,
 202 is critical as the 'worldSEQ' operation is unsafe if the token can be
 203 duplicated!!!
 204
 205 \begin{code}
 206 type SubstArray = _MutableArray _RealWorld Int (Maybe TauType)
 207
 208 type SubstArrayIndex = Int      -- Allocated within this module, single-threadedly
 209
 210 data Subst
 211   = MkSubst SubstArray          -- Mapping for allocated tyvars
 212
 213             [(SubstArrayIndex, Bag (SubstArrayIndex, Maybe TauType))]
 214                                 -- Stack to be undone if we fail, plus next free
 215                                 -- slot when reverting.  All the undos are for
 216                                 -- slots earlier than the corresp "next free" index.
 217                                 --
 218                                 -- The "bag" is a lie: it's really a sequence, with
 219                                 -- the most recently performed write appearing first.
 220
 221             STWorld             -- State token
 222
 223             SubstArrayIndex     -- Next free slot
 224 \end{code}
 225
 226 Here's a local monad for threading the substitution around:
 227
 228 \begin{code}
 229 type SubstM a = Subst -> (Subst,a)
 230
 231 returnSubstM x = \s -> (s,x)
 232 thenSubstM m k = \s -> case m s of { (s1, r) -> k r s1 }
 233
 234 mapSubstM f []     = returnSubstM []
 235 mapSubstM f (x:xs) = f x                `thenSubstM` \ r ->
 236                      mapSubstM f xs     `thenSubstM` \ rs ->
 237                      returnSubstM (r:rs)
 238
 239 -- Breaks the ST abstraction.  But we have to do so somewhere...
 240 doST :: STWorld -> ST _RealWorld a -> (a, STWorld)
 241 doST w st = st w
 242 \end{code}
 243
 244 %********************************************************
 245 %*                                                      *
 246 \subsubsection{@Subst@: the array}
 247 %*                                                      *
 248 %********************************************************
 249
 250 \begin{code}
 251 writeSubst  :: SubstArrayIndex -> Maybe TauType -> SubstM ()
 252         -- writeSubst writes in such a way that we can undo it later
 253
 254 writeSubst index new_val
 255            (MkSubst arr undo_stack@((checkpoint, undos):rest_undo_stack)
 256                     world next_free)
 257   | index < checkpoint  -- Record in undos
 258   = let
 259         (old, new_world) = doST world (
 260                           readArray arr index           `thenStrictlyST` \ old_val ->
 261                           writeArray arr index new_val  `seqStrictlyST`
 262                           returnStrictlyST old_val
 263                         )
 264         new_undos = unitBag (index,old) `unionBags` undos
 265                         -- The order is significant!  The right most thing
 266                         -- gets undone last
 267     in
 268     (MkSubst arr ((checkpoint, new_undos) : rest_undo_stack) new_world next_free, ())
 269
 270 writeSubst index new_val (MkSubst arr undo_stack world next_free)
 271   -- No need to record in undos: undo_stack is empty,
 272   -- or index is after checkpoint
 273   = let
 274         (_, new_world) = doST world (writeArray arr index new_val)
 275     in
 276     (MkSubst arr undo_stack new_world next_free, ())
 277
 278 readSubst  :: SubstArrayIndex -> SubstM (Maybe TauType)
 279 readSubst index (MkSubst arr undos world supplies)
 280   = let
 281         (result, new_world) = doST world (readArray arr index)
 282     in
 283     (MkSubst arr undos new_world supplies, result)
 284
 285 tyVarToIndex :: TyVar -> SubstArrayIndex
 286 tyVarToIndex tyvar = unpkUnifiableTyVarUnique (getTheUnique tyvar)
 287 \end{code}
 288
 289 %********************************************************
 290 %*                                                      *
 291 \subsubsection{@Subst@: building them}
 292 %*                                                      *
 293 %********************************************************
 294
 295 The function @mkEmptySubst@ used to be a CAF containing a mutable
 296 array.  The imperative world had a name for this kind of thing:
 297 ``global variable'' and has observed that using these ``global variables''
 298 leads to something they call ``side effects''.
 299
 300 These ``side effects'' never caused a problem for @hsc@ because empty
 301 substitutions are only used in one place (the typechecker) and only
 302 used once in every program run.  In \tr{ghci} however, we might use the
 303 typechecker several times---in which case we'd like to have a
 304 different (fresh) substitution each time.  The easy way (HACK) to
 305 achieve this is to deCAFinate so that a fresh substitution will be
 306 created each time the typechecker runs.
 307
 308 \begin{code}
 309 aRRAY_START :: Int
 310 aRRAY_START = 0
 311
 312 mkEmptySubst aRRAY_SIZE
 313   = let
 314         world = newWorld (S# realWorld#)
 315         (arr, new_world) = doST world (newArray (aRRAY_START,aRRAY_SIZE) Nothing)
 316     in
 317     MkSubst arr [] new_world aRRAY_START
 318
 319 extendSubstArr :: Subst
 320                -> Subst
 321 extendSubstArr (MkSubst old_arr undos world next_free)
 322   = let
 323         -- these "sizes" are really end-limits (WDP 94/11)
 324         cur_size  = case (boundsOfArray old_arr) of { (_, x) -> x }
 325         new_size = (cur_size * 2) + 1
 326
 327         (new_arr, new_world) = doST world (
 328                                 newArray (aRRAY_START,new_size) Nothing `thenStrictlyST` \ new_arr ->
 329                                 let
 330                                     copyArr pos
 331                                         | pos > cur_size = returnStrictlyST ()
 332                                         | otherwise
 333                                           = readArray  old_arr pos      `thenStrictlyST`  \ ele ->
 334                                             writeArray new_arr pos ele  `seqStrictlyST`
 335                                             copyArr (pos + 1)
 336                                 in
 337                                 copyArr aRRAY_START             `seqStrictlyST`
 338                                 returnStrictlyST new_arr
 339                             )
 340     in
 341     MkSubst new_arr undos new_world next_free
 342 \end{code}
 343
 344 \begin{code}
 345 extendSubst tyvar tau_ty
 346   = readSubst index             `thenSubstM` \ maybe_ty ->
 347
 348     case maybe_ty of
 349        Just exist_ty -> -- Bound already
 350                 returnSubstM (AlreadyBound exist_ty)
 351
 352        Nothing       -> -- Not already bound
 353           apply_rep_to_ty tau_ty `thenSubstM` \ new_tau_ty ->
 354           case expandVisibleTySyn new_tau_ty of
 355                 UniTyVar tv | tv `eqTyVar` tyvar ->
 356                         -- Trivial new binding of a type variable to itself;
 357                         -- return old substition
 358                        returnSubstM SubstOK
 359
 360                 other | tyvar `is_elem`  (extractTyVarsFromTy new_tau_ty) ->
 361                         -- Occurs check finds error
 362                         returnSubstM (OccursCheck tyvar new_tau_ty)
 363
 364                       | otherwise ->
 365                         -- OK to bind
 366                         writeSubst index (Just new_tau_ty) `thenSubstM` \ _ ->
 367                         returnSubstM SubstOK
 368   where
 369       index   = tyVarToIndex tyvar
 370       is_elem = isIn "extendSubst"
 371 \end{code}
 372
 373 %********************************************************
 374 %*                                                      *
 375 \subsubsection{@Subst@: lookup}
 376 %*                                                      *
 377 %********************************************************
 378
 379 All of them use the underlying function, @apply_rep_to_ty@, which
 380 ensures that an idempotent result is returned.
 381
 382 \begin{code}
 383 applySubstToTy      subst ty       = apply_rep_to_ty ty subst
 384 applySubstToTauTy   subst tau_ty   = apply_rep_to_ty tau_ty subst
 385 applySubstToTyVar   subst tyvar    = apply_rep_to_ty (mkTyVarTy tyvar) subst
 386 applySubstToThetaTy subst theta_ty
 387   = let
 388       do_one (clas, ty) = apply_rep_to_ty ty  `thenSubstM` \ new_ty ->
 389                           returnSubstM (clas, new_ty)
 390     in
 391     mapSubstM do_one theta_ty subst
 392 \end{code}
 393
 394 And now down to serious business...
 395 \begin{code}
 396 apply_rep_to_ty :: UniType -> SubstM UniType
 397
 398 apply_rep_to_ty (UniTyVar tyvar)
 399   = readSubst index             `thenSubstM` \ maybe_ty ->
 400     case maybe_ty of
 401
 402       Nothing -> -- Not found, so return a trivial type
 403                  returnSubstM (mkTyVarTy tyvar)
 404
 405       Just ty -> -- Found, so recursively apply the subst the result to
 406                  -- maintain idempotence!
 407                  apply_rep_to_ty ty             `thenSubstM` \ new_ty ->
 408
 409                  -- The mapping for this tyvar is then updated with the
 410                  -- result to reduce the number of subsequent lookups
 411                  writeSubst index (Just new_ty) `thenSubstM` \ _ ->
 412
 413                  returnSubstM new_ty
 414   where
 415     index = tyVarToIndex tyvar
 416
 417 apply_rep_to_ty (UniFun t1 t2)
 418   = apply_rep_to_ty t1          `thenSubstM` \ new_t1 ->
 419     apply_rep_to_ty t2          `thenSubstM` \ new_t2 ->
 420     returnSubstM (UniFun new_t1 new_t2)
 421
 422 apply_rep_to_ty (UniData con args)
 423   = mapSubstM apply_rep_to_ty args      `thenSubstM` \ new_args ->
 424     returnSubstM (UniData con new_args)
 425
 426 apply_rep_to_ty (UniSyn con args ty)
 427   = mapSubstM apply_rep_to_ty args      `thenSubstM` \ new_args ->
 428     apply_rep_to_ty ty                  `thenSubstM` \ new_ty ->
 429     returnSubstM (UniSyn con new_args new_ty)
 430
 431 apply_rep_to_ty (UniDict clas ty)
 432   = apply_rep_to_ty ty          `thenSubstM` \ new_ty ->
 433     returnSubstM (UniDict clas new_ty)
 434
 435 apply_rep_to_ty (UniForall v ty)
 436   = apply_rep_to_ty ty          `thenSubstM` \ new_ty ->
 437     returnSubstM (UniForall v new_ty)
 438
 439 apply_rep_to_ty ty@(UniTyVarTemplate v) = returnSubstM ty
 440 \end{code}
 441
 442 %************************************************************************
 443 %*                                                                      *
 444 \subsubsection{Allocating @TyVarUniques@}
 445 %*                                                                      *
 446 %************************************************************************
 447
 448 The array is extended if the allocated type variables would cause an
 449 out of bounds error.
 450
 451 \begin{code}
 452 getSubstTyVarUnique subst@(MkSubst arr undo world next_free)
 453   | next_free <= size   -- The common case; there's a spare slot
 454   = (MkSubst arr undo world new_next_free, uniq)
 455
 456   | otherwise           -- Need more room: Extend first, then re-try
 457   = getSubstTyVarUnique (extendSubstArr subst)
 458
 459   where
 460     size       = case (boundsOfArray arr) of { (_, x) -> x  }
 461     uniq       = mkUnifiableTyVarUnique next_free
 462     new_next_free = next_free + 1
 463
 464
 465 getSubstTyVarUniques n subst@(MkSubst arr undo world next_free)
 466   | new_next_free - 1 <= size   -- The common case; there's a spare slot
 467   = (MkSubst arr undo world new_next_free, uniqs)
 468
 469   | otherwise           -- Need more room: extend, then re-try
 470   = getSubstTyVarUniques n (extendSubstArr subst)
 471
 472   where
 473     size        = case (boundsOfArray arr) of { (_, x) -> x  }
 474     uniqs       = [mkUnifiableTyVarUnique (next_free + i) | i <- [0..n-1]]
 475     new_next_free  = next_free + n
 476 \end{code}
 477
 478 %************************************************************************
 479 %*                                                                      *
 480 \subsubsection{Undoing substitution on typechecking failure}
 481 %*                                                                      *
 482 %************************************************************************
 483
 484 \begin{code}
 485 pushSubstUndos (MkSubst arr undos world next_free)
 486   = MkSubst arr ((next_free,emptyBag):undos) world next_free
 487
 488 combineSubstUndos (MkSubst arr [_] world next_free)
 489   = MkSubst arr [] world next_free  -- top level undo ignored
 490
 491 combineSubstUndos (MkSubst arr ((_,u1):(checkpoint,u2):undo_stack)
 492                            world next_free)
 493   = MkSubst arr ((checkpoint, new_u1 `unionBags` u2):undo_stack) world next_free
 494   where
 495         -- Keep only undos which apply to indices before checkpoint
 496     new_u1 = filterBag (\ (index,val) -> index < checkpoint) u1
 497
 498 undoSubstUndos (MkSubst arr ((checkpoint,undo_now):undo_stack) world next_free)
 499   = MkSubst arr undo_stack new_world checkpoint
 500   where
 501     (_, new_world) = doST world (perform_undo (bagToList undo_now) `seqStrictlyST`
 502                               clear_block checkpoint
 503                              )
 504
 505     perform_undo []                  = returnStrictlyST ()
 506     perform_undo ((index,val):undos) = writeArray arr index val `seqStrictlyST`
 507                                        perform_undo undos
 508
 509         -- (clear_block n) clears the array from n up to next_free
 510         -- This is necessary because undos beyond supp2 aren't recorded in undos
 511     clear_block n | n >= next_free = returnStrictlyST ()
 512                   | otherwise      = writeArray arr n Nothing `seqStrictlyST`
 513                                      clear_block (n+1)
 514 \end{code}
 515
 516 %************************************************************************
 517 %*                                                                      *
 518 \subsubsection{Pruning a substitution}
 519 %*                                                                      *
 520 %************************************************************************
 521
 522 ToDo: Implement with array !!  Ignore?  Restore unique supply?
 523
 524 @pruneSubst@ prunes a substitution to a given level.
 525
 526 This is tricky stuff.  The idea is that if we
 527     (a) catch the current unique supply
 528     (b) do some work
 529     (c) back-substitute over the results of the work
 530     (d) prune the substitution back to the level caught in (a)
 531 then everything will be fine.  Any *subsequent* unifications to
 532 these just-pruned ones will be added and not subsequently deleted.
 533
 534 NB: this code relies on the idempotence property, otherwise discarding
 535 substitions might be dangerous.
 536
 537 \begin{code}
 538 {-
 539 pruneSubst :: TyVarUnique -> Subst -> Subst
 540
 541 pruneSubst keep_marker (MkSubst subst_rep)
 542   = -- BSCC("pruneSubst")
 543     MkSubst [(tyvar,ty) | (tyvar,ty) <- subst_rep,
 544              getTheUnique tyvar `ltUnique` keep_marker]
 545     -- ESCC
 546 -}
 547 \end{code}
 548
 549 %************************************************************************
 550 %*                                                                      *
 551 \subsection[Subst-Lists]{@Subst@ with poor list implementation}
 552 %*                                                                      *
 553 %************************************************************************
 554
 555 If don't have Glasgow Haskell we have to revert to list implementation
 556 of arrays ...
 557
 558 \begin{code}
 559 #else {- ! __GLASGOW_HASKELL__ -}
 560 \end{code}
 561
 562 %************************************************************************
 563 %*                                                                      *
 564 \subsubsection{@Subst@: specification and representation}
 565 %*                                                                      *
 566 %************************************************************************
 567
 568 {\em Specification:}
 569 * When new bindings are added to the substitution, an occurs check is performed.
 570 * The applySubst function guarantees to return a fixed point of the substitution.
 571
 572 {\em Representation:}
 573 A substitution binds type variables to tau-types, that is @UniType@s without
 574 any @UniForall@ or @UniDict@ constructors.
 575
 576 It is represented as an association list, indexed on Uniques
 577 with a stack of type variable unique markers indicating undo
 578 checkpoints.  The supply of TyVarUniques is also part of the
 579 aubstitution.
 580
 581 The undo information is a stack of tyvar markers. If the typecheck
 582 fails all extensions to the association list subsequent to (and
 583 including) the marker are undone. If it succeeds the current marker is
 584 discarded.
 585
 586 The unique supply is also stacked so that it can be restored if a
 587 typecheck fails.
 588
 589 \begin{code}
 590 type SubstRep = [(Unique, TauType)]
 591
 592 data Subst
 593   = MkSubst SubstRep            -- mapping for allocated tyvars
 594             [Maybe Unique]      -- stack of markers to strip off if we fail
 595             [UniqueSupply]      -- stack of tyvar unique supplies
 596
 597 mkEmptySubst size = MkSubst [] [] []
 598 \end{code}
 599
 600 \begin{code}
 601 lookup_rep :: SubstRep -> TyVar -> Maybe TauType
 602 lookup_rep alist tyvar
 603   = let
 604         key = getTheUnique tyvar
 605
 606         lookup []            = Nothing
 607         lookup ((u,ty):rest)
 608           = case (cmpUnique key u) of { EQ_ -> Just ty; _ -> lookup rest }
 609     in
 610     lookup alist
 611 \end{code}
 612
 613 %********************************************************
 614 %*                                                      *
 615 \subsubsection{@Subst@: building them}
 616 %*                                                      *
 617 %********************************************************
 618
 619 \begin{code}
 620 --OLD? initSubst init = MkSubst [] [] [mkUniqueSupply init]
 621 \end{code}
 622
 623 \begin{code}
 624 extendSubst subst@(MkSubst srep undo supp) tyvar tau_ty
 625   = -- BSCC("extendSubst")
 626     apply_rep_to_ty srep tau_ty `thenLft` \ new_tau_ty ->
 627
 628     case expandVisibleTySyn new_tau_ty of
 629
 630         UniTyVar tv | tv `eqTyVar` tyvar ->
 631              -- Trivial new binding; return old substition
 632              (SubstOK, subst)
 633
 634         _ -> let
 635                 is_elem = isIn "extendSubst2"
 636              in
 637              if (tyvar `is_elem` (extractTyVarsFromTy new_tau_ty)) then
 638                  (OccursCheck tyvar new_tau_ty, subst)
 639              else
 640                  case lookup_rep srep tyvar of
 641                      Just exist_ty ->
 642                          (AlreadyBound exist_ty, subst)
 643                      Nothing       ->
 644                          let
 645                            new_srep = (getTheUnique tyvar, new_tau_ty) : srep
 646                            new_undo = case undo of
 647                                       []                -> []
 648                                           -- top level undo ignored
 649
 650                                       (Nothing : undos) -> (Just (getTheUnique tyvar)) : undos
 651                                       (Just _ : _ )     -> undo
 652                                           -- only first undo recorded
 653                          in
 654                          (SubstOK, MkSubst new_srep new_undo supp)
 655     -- ESCC
 656 \end{code}
 657
 658 %********************************************************
 659 %*                                                      *
 660 \subsubsection{@Subst@: lookup}
 661 %*                                                      *
 662 %********************************************************
 663
 664 All of them use the underlying function, @apply_rep_to_ty@, which
 665 ensures that an idempotent result is returned.
 666
 667 \begin{code}
 668 applySubstToTy subst@(MkSubst srep undo supp) ty
 669   = -- BSCC("applySubstToTy")
 670     apply_rep_to_ty srep ty             `thenLft` \ new_ty ->
 671     (subst, new_ty)
 672     -- ESCC
 673
 674 applySubstToTauTy subst@(MkSubst srep undo supp) tauty
 675   = -- BSCC("applySubstToTauTy")
 676     apply_rep_to_ty srep tauty          `thenLft`\ new_tauty ->
 677         (subst, new_tauty)
 678     -- ESCC
 679
 680 applySubstToThetaTy subst@(MkSubst srep undo supp) theta
 681   = -- BSCC("applySubstToThetaTy")
 682     let
 683         do_one (clas, ty) = apply_rep_to_ty srep ty  `thenLft` \ new_ty ->
 684                             returnLft (clas, new_ty)
 685     in
 686     mapLft do_one theta         `thenLft` \ new_theta ->
 687     (subst, new_theta)
 688     -- ESCC
 689
 690 applySubstToTyVar subst@(MkSubst srep undo supp) tyvar
 691   = -- BSCC("applySubstToTyVar")
 692     apply_rep_to_ty srep (mkTyVarTy tyvar) `thenLft` \ new_tauty ->
 693     (subst, new_tauty)
 694     -- ESCC
 695 \end{code}
 696
 697 And now down to serious business...
 698 \begin{code}
 699 apply_rep_to_ty :: SubstRep -> UniType -> LiftM UniType
 700
 701 apply_rep_to_ty srep (UniTyVar tyvar)
 702   = case lookup_rep srep tyvar of
 703       Nothing -> -- Not found, so return a trivial type
 704                  returnLft (mkTyVarTy tyvar)
 705
 706       Just ty -> -- Found, so recursively apply the subst the result to
 707                  -- maintain idempotence!
 708                  apply_rep_to_ty srep ty
 709
 710 apply_rep_to_ty srep (UniFun t1 t2)
 711   = apply_rep_to_ty srep t1             `thenLft` \ new_t1 ->
 712     apply_rep_to_ty srep t2             `thenLft` \ new_t2 ->
 713     returnLft (UniFun new_t1 new_t2)
 714
 715 apply_rep_to_ty srep (UniData con args)
 716   = mapLft (apply_rep_to_ty srep) args  `thenLft` \ new_args ->
 717     returnLft (UniData con new_args)
 718
 719 apply_rep_to_ty srep (UniSyn con args ty)
 720   = mapLft (apply_rep_to_ty srep) args  `thenLft` \ new_args ->
 721     apply_rep_to_ty srep ty             `thenLft` \ new_ty ->
 722     returnLft (UniSyn con new_args new_ty)
 723
 724 apply_rep_to_ty srep (UniDict clas ty)
 725   = apply_rep_to_ty srep ty             `thenLft` \ new_ty ->
 726     returnLft (UniDict clas new_ty)
 727
 728 apply_rep_to_ty srep (UniForall v ty)
 729   = apply_rep_to_ty srep ty             `thenLft` \ new_ty ->
 730     returnLft (UniForall v new_ty)
 731
 732 apply_rep_to_ty srep ty@(UniTyVarTemplate v) =  returnLft ty
 733 \end{code}
 734
 735 %************************************************************************
 736 %*                                                                      *
 737 \subsubsection{Allocating TyVarUniques}
 738 %*                                                                      *
 739 %************************************************************************
 740
 741 The array is extended if the allocated type variables would cause an
 742 out of bounds error.
 743
 744 \begin{code}
 745 getSubstTyVarUnique subst@(MkSubst srep undo (supp:supps))
 746   = -- BSCC("allocTyVarUniques")
 747     case getUnique supp of
 748       (new_supp, uniq) -> (MkSubst srep undo (new_supp:supps), uniq)
 749     -- ESCC
 750
 751 getSubstTyVarUniques n subst@(MkSubst srep undo (supp:supps))
 752   = -- BSCC("allocTyVarUniques")
 753     case getUniques n supp of
 754       (new_supp, uniqs) -> (MkSubst srep undo (new_supp:supps), uniqs)
 755     -- ESCC
 756 \end{code}
 757
 758 %************************************************************************
 759 %*                                                                      *
 760 \subsubsection[Subst-undo]{Undoing substitution on typechecking failure}
 761 %*                                                                      *
 762 %************************************************************************
 763
 764 \begin{code}
 765 pushSubstUndos subst@(MkSubst srep undos (supp:supps))
 766   = -- BSCC("pushSubstUndos")
 767     MkSubst srep (Nothing:undos) (supp:supp:supps)
 768     -- ESCC
 769
 770 combineSubstUndos subst@(MkSubst srep (u:us) (supp1:supp2:supps))
 771   = -- BSCC("combineSubstUndos")
 772       MkSubst srep us (supp1:supps)
 773     -- ESCC
 774
 775 undoSubstUndos subst@(MkSubst srep (u:us) (supp1:supp2:supps))
 776   = -- BSCC("undoSubstUndos")
 777     let
 778       strip_to []            key = []
 779       strip_to ((u,ty):srep) key
 780         = case (cmpUnique u key) of { EQ_ -> srep; _ -> strip_to srep key }
 781
 782       perform_undo Nothing     srep = srep
 783       perform_undo (Just uniq) srep = strip_to srep uniq
 784     in
 785       MkSubst (perform_undo u srep) us (supp2:supps)
 786
 787         -- Note: the saved unique supply is restored from the enclosing scope
 788
 789     -- ESCC
 790 \end{code}
 791
 792 %************************************************************************
 793 %*                                                                      *
 794 \subsubsection{Pruning a substitution}
 795 %*                                                                      *
 796 %************************************************************************
 797
 798 ToDo: Implement with list !!  Ignore?  Restore unique supply?
 799
 800 @pruneSubst@ prunes a substitution to a given level.
 801
 802 This is tricky stuff.  The idea is that if we
 803     (a) catch the current unique supply
 804     (b) do some work
 805     (c) back-substitute over the results of the work
 806     (d) prune the substitution back to the level caught in (a)
 807 then everything will be fine.  Any *subsequent* unifications to
 808 these just-pruned ones will be added and not subsequently deleted.
 809
 810 NB: this code relies on the idempotence property, otherwise discarding
 811 substitions might be dangerous.
 812
 813 \begin{code}
 814 {-
 815 pruneSubst :: TyVarUnique -> Subst -> Subst
 816
 817 pruneSubst keep_marker (MkSubst subst_rep)
 818   = -- BSCC("pruneSubst")
 819     MkSubst [(tyvar,ty) | (tyvar,ty) <- subst_rep,
 820              getTheUnique tyvar `ltUnique` keep_marker]
 821     -- ESCC
 822 -}
 823 \end{code}
 824
 825 \begin{code}
 826 #endif {- ! __GLASGOW_HASKELL__ -}
 827 \end{code}