src/tycheck.sml

   1 (* HCoop Domtool (http://hcoop.sourceforge.net/)
   2  * Copyright (c) 2006, Adam Chlipala
   3  *
   4  * This program is free software; you can redistribute it and/or
   5  * modify it under the terms of the GNU General Public License
   6  * as published by the Free Software Foundation; either version 2
   7  * of the License, or (at your option) any later version.
   8  *
   9  * This program is distributed in the hope that it will be useful,
  10  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  11  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  12  * GNU General Public License for more details.
  13  *
  14  * You should have received a copy of the GNU General Public License
  15  * along with this program; if not, write to the Free Software
  16  * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
  17  *)
  18
  19 (* Domtool configuration language type checking *)
  20
  21 structure Tycheck :> TYCHECK = struct
  22
  23 open Ast Print Env
  24
  25 structure SM = StringMap
  26
  27 local
  28     val unifCount = ref 0
  29 in
  30 fun resetUnif () = unifCount := 0
  31
  32 fun newUnif () =
  33     let
  34         val c = !unifCount
  35         val name =
  36             if c < 26 then
  37                 str (chr (ord #"A" + c))
  38             else
  39                 "UNIF" ^ Int.toString (c - 26)
  40     in
  41         unifCount := c + 1;
  42         TUnif (name, ref NONE)
  43     end
  44 end
  45
  46 exception UnequalDomains
  47
  48 fun eqRecord f (r1, r2) =
  49     (SM.appi (fn (k, v1) =>
  50                  case SM.find (r2, k) of
  51                      NONE => raise UnequalDomains
  52                    | SOME v2 =>
  53                      if f (v1, v2) then
  54                          ()
  55                      else
  56                          raise UnequalDomains) r1;
  57      SM.appi (fn (k, v2) =>
  58                  case SM.find (r1, k) of
  59                      NONE => raise UnequalDomains
  60                    | SOME v1 =>
  61                      if f (v1, v2) then
  62                          ()
  63                      else
  64                          raise UnequalDomains) r2;
  65      true)
  66     handle UnequalDomains => false
  67
  68 fun eqPred ((p1, _), (p2, _)) =
  69     case (p1, p2) of
  70         (CRoot, CRoot) => true
  71       | (CConst s1, CConst s2) => s1 = s2
  72       | (CPrefix p1, CPrefix p2) => eqPred (p1, p2)
  73       | (CNot p1, CNot p2) => eqPred (p1, p2)
  74       | (CAnd (p1, q1), CAnd (p2, q2)) =>
  75         eqPred (p1, p2) andalso eqPred (q1, q2)
  76
  77       | _ => false
  78
  79 fun eqTy (t1All as (t1, _), t2All as (t2, _)) =
  80     case (t1, t2) of
  81         (TBase s1, TBase s2) => s1 = s2
  82       | (TList t1, TList t2) => eqTy (t1, t2)
  83       | (TArrow (d1, r1), TArrow (d2, r2)) =>
  84         eqTy (d1, d2) andalso eqTy (r1, r2)
  85
  86       | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
  87         eqPred (p1, p2) andalso eqRecord eqTy (d1, d2)
  88         andalso eqRecord eqTy (r1, r2)
  89
  90       | (TNested (p1, q1), TNested (p2, q2)) =>
  91         eqPred (p1, p2) andalso eqTy (q1, q2)
  92
  93       | (TUnif (_, ref (SOME t1)), _) => eqTy (t1, t2All)
  94       | (_, TUnif (_, ref (SOME t2))) => eqTy (t1All, t2)
  95
  96       | (TUnif (_, r1), TUnif (_, r2)) => r1 = r2
  97
  98       | (TError, TError) => true
  99
 100       | _ => false
 101
 102 datatype unification_error =
 103          UnifyPred of pred * pred
 104        | UnifyTyp of typ * typ
 105        | UnifyOccurs of string * typ
 106
 107 exception Unify of unification_error
 108
 109 datatype type_error =
 110          WrongType of string * exp * typ * typ * unification_error option
 111        | WrongForm of string * string * exp * typ * unification_error option
 112        | UnboundVariable of string
 113        | WrongPred of string * pred * pred
 114
 115 fun describe_unification_error t ue =
 116     case ue of
 117         UnifyPred (p1, p2) =>
 118         (print "Reason: Incompatible contexts.\n";
 119          preface ("Have:", p_pred p1);
 120          preface ("Need:", p_pred p2))
 121       | UnifyTyp (t1, t2) =>
 122         if eqTy (t, t1) then
 123             ()
 124         else
 125             (print "Reason: Incompatible types.\n";
 126              preface ("Have:", p_typ t1);
 127              preface ("Need:", p_typ t2))
 128       | UnifyOccurs (name, t') =>
 129         if eqTy (t, t') then
 130             ()
 131         else
 132             (print "Reason: Occurs check failed for ";
 133              print name;
 134              print " in:\n";
 135              printd (p_typ t))
 136
 137 fun describe_type_error loc te =
 138     case te of
 139         WrongType (place, e, t1, t2, ueo) =>
 140         (ErrorMsg.error (SOME loc) (place ^ " has wrong type.");
 141          preface (" Expression:", p_exp e);
 142          preface ("Actual type:", p_typ t1);
 143          preface ("Needed type:", p_typ t2);
 144          Option.app (describe_unification_error t1) ueo)
 145       | WrongForm (place, form, e, t, ueo) =>
 146         (ErrorMsg.error (SOME loc) (place ^ " has a non-" ^ form ^ " type.");
 147          preface ("Expression:", p_exp e);
 148          preface ("      Type:", p_typ t);
 149          Option.app (describe_unification_error t) ueo)
 150       | UnboundVariable name =>
 151         ErrorMsg.error (SOME loc) ("Unbound variable " ^ name ^ ".\n")
 152       | WrongPred (place, p1, p2) =>
 153         (ErrorMsg.error (SOME loc) ("Context incompatibility for " ^ place ^ ".");
 154          preface ("Have:", p_pred p1);
 155          preface ("Need:", p_pred p2))
 156
 157 fun predImplies (p1All as (p1, _), p2All as (p2, _)) =
 158     case (p1, p2) of
 159         (_, CAnd (p1, p2)) => predImplies (p1All, p1) andalso predImplies (p1All, p2)
 160       | (CAnd (p1, p2), _) => predImplies (p1, p2All) orelse predImplies (p2, p2All)
 161
 162       | (_, CPrefix (CRoot, _)) => true
 163       | (CNot (CPrefix (CRoot, _), _), _) => true
 164
 165       | (CRoot, CRoot) => true
 166
 167       | (CConst s1, CConst s2) => s1 = s2
 168
 169       | (CPrefix p1, CPrefix p2) => predImplies (p1, p2)
 170       | (_, CPrefix p2) => predImplies (p1All, p2)
 171
 172       | (CNot p1, CNot p2) => predImplies (p2, p1)
 173
 174       | _ => false
 175
 176 fun predSimpl (pAll as (p, loc)) =
 177     case p of
 178         CRoot => pAll
 179       | CConst _ => pAll
 180       | CPrefix p => (CPrefix (predSimpl p), loc)
 181       | CNot p => (CNot (predSimpl p), loc)
 182       | CAnd (p1, p2) =>
 183         let
 184             val p1' = predSimpl p1
 185             val p2' = predSimpl p2
 186         in
 187             case p1' of
 188                 (CAnd (c1, c2), _) => predSimpl (CAnd (c1, (CAnd (c2, p2'), loc)), loc)
 189               | _ => if predImplies (p2', p1') then
 190                          p2'
 191                      else if predImplies (p1', p2') then
 192                          p1'
 193                      else
 194                          (CAnd (p1', p2'), loc)
 195         end
 196
 197 fun subPred (p1, p2) =
 198     if predImplies (p1, p2) then
 199         ()
 200     else
 201         raise (Unify (UnifyPred (p1, p2)))
 202
 203 fun subRecord f (r1, r2) =
 204     SM.appi (fn (k, v2) =>
 205                 case SM.find (r1, k) of
 206                     NONE => raise UnequalDomains
 207                   | SOME v1 => f (v1, v2)) r2
 208
 209 fun occurs u (t, _) =
 210     case t of
 211         TBase _ => false
 212       | TList t => occurs u t
 213       | TArrow (d, r) => occurs u d orelse occurs u r
 214       | TAction (_, d, r) =>
 215         List.exists (occurs u) (SM.listItems d)
 216         orelse List.exists (occurs u) (SM.listItems r)
 217       | TNested (_, t) => occurs u t
 218       | TError => false
 219       | TUnif (_, ref (SOME t)) => occurs u t
 220       | TUnif (_, u') => u = u'
 221
 222 fun subTyp (t1All as (t1, _), t2All as (t2, _)) =
 223     case (t1, t2) of
 224         (TBase s1, TBase s2) =>
 225         if s1 = s2 then
 226             ()
 227         else
 228             raise Unify (UnifyTyp (t1All, t2All))
 229       | (TList t1, TList t2) => subTyp (t1, t2)
 230       | (TArrow (d1, r1), TArrow (d2, r2)) =>
 231         (subTyp (d2, d1);
 232          subTyp (r1, r2))
 233
 234       | (TAction (p1, d1, r1), TAction (p2, d2, r2)) =>
 235         ((subPred (p2, p1);
 236           subRecord subTyp (d2, d1);
 237           subRecord subTyp (r1, r2);
 238           subRecord subTyp (r2, r1))
 239          handle UnequalDomains => raise Unify (UnifyTyp (t1All, t2All)))
 240
 241       | (TNested (d1, r1), TNested (d2, r2)) =>
 242         (subPred (d2, d1);
 243          subTyp (r1, r2))
 244
 245       | (TUnif (_, ref (SOME t1)), _) => subTyp (t1, t2All)
 246       | (_, TUnif (_, ref (SOME t2))) => subTyp (t1All, t2)
 247
 248       | (TUnif (_, r1), TUnif (_, r2)) =>
 249         if r1 = r2 then
 250             ()
 251         else
 252             r1 := SOME t2All
 253
 254       | (TUnif (name, r), _) =>
 255         if occurs r t2All then
 256             raise (Unify (UnifyOccurs (name, t2All)))
 257         else
 258             r := SOME t2All
 259
 260       | (_, TUnif (name, r)) =>
 261         if occurs r t1All then
 262             raise (Unify (UnifyOccurs (name, t1All)))
 263         else
 264             r := SOME t1All
 265
 266       | (TError, _) => ()
 267       | (_, TError) => ()
 268
 269       | _ => raise Unify (UnifyTyp (t1All, t2All))
 270
 271 fun isError t =
 272     case t of
 273         (TError, _) => true
 274       | _ => false
 275
 276 fun whnorm (tAll as (t, loc)) =
 277     case t of
 278         TUnif (_, ref (SOME tAll)) => whnorm tAll
 279       | _ => tAll
 280
 281 fun baseCondition t =
 282     case whnorm t of
 283         (TBase name, _) => typeRule name
 284       | (TList t, _) =>
 285         (case baseCondition t of
 286              NONE => NONE
 287            | SOME f => SOME (fn (EList ls, _) => List.all f ls
 288                               | _ => false))
 289       | _ => NONE
 290
 291 fun hasTyp (e, t1, t2) =
 292     if (case baseCondition t2 of
 293             NONE => false
 294           | SOME rule => rule e) then
 295         ()
 296     else
 297         subTyp (t1, t2)
 298
 299 fun checkPred G (p, loc) =
 300     let
 301         val err = ErrorMsg.error (SOME loc)
 302     in
 303         case p of
 304             CRoot => ()
 305           | CConst s =>
 306             if lookupContext G s then
 307                 ()
 308             else
 309                 err ("Unbound context " ^ s)
 310           | CPrefix p => checkPred G p
 311           | CNot p => checkPred G p
 312           | CAnd (p1, p2) => (checkPred G p1; checkPred G p2)
 313     end
 314
 315 fun checkTyp G (tAll as (t, loc)) =
 316     let
 317         val err = ErrorMsg.error (SOME loc)
 318     in
 319         case t of
 320             TBase name =>
 321             if lookupType G name then
 322                 tAll
 323             else
 324                 (err ("Unbound type name " ^ name);
 325                  (TError, loc))
 326           | TList t => (TList (checkTyp G t), loc)
 327           | TArrow (d, r) => (TArrow (checkTyp G d, checkTyp G r), loc)
 328           | TAction (p, d, r) => (checkPred G p;
 329                                   (TAction (p, SM.map (checkTyp G) d,
 330                                             SM.map (checkTyp G) r), loc))
 331           | TNested (p, t) => (checkPred G p;
 332                                (TNested (p, checkTyp G t), loc))
 333           | TError => raise Fail "TError in parser-generated type"
 334           | TUnif _ => raise Fail "TUnif in parser-generated type"
 335     end
 336
 337 fun checkExp G (eAll as (e, loc)) =
 338     let
 339         val dte = describe_type_error loc
 340     in
 341         case e of
 342             EInt _ => (TBase "int", loc)
 343           | EString _ => (TBase "string", loc)
 344           | EList es =>
 345             let
 346                 val t = (newUnif (), loc)
 347             in
 348                 foldl (fn (e', ret) =>
 349                           let
 350                               val t' = checkExp G e'
 351                           in
 352                               (hasTyp (eAll, t', t);
 353                                if isError t' then
 354                                    (TList (TError, loc), loc)
 355                                else
 356                                    ret)
 357                               handle Unify ue =>
 358                                      (dte (WrongType ("List element",
 359                                                       e',
 360                                                       t',
 361                                                       t,
 362                                                       SOME ue));
 363                                       (TError, loc))
 364                           end) (TList t, loc) es
 365             end
 366
 367           | ELam (x, to, e) =>
 368             let
 369                 val t =
 370                     case to of
 371                         NONE => (newUnif (), loc)
 372                       | SOME t => checkTyp G t
 373
 374                 val G' = bindVal G (x, t, NONE)
 375                 val t' = checkExp G' e
 376             in
 377                 (TArrow (t, t'), loc)
 378             end
 379           | EVar x =>
 380             (case lookupVal G x of
 381                  NONE => (dte (UnboundVariable x);
 382                           (TError, loc))
 383                | SOME t => t)
 384           | EApp (func, arg) =>
 385             let
 386                 val dom = (newUnif (), loc)
 387                 val ran = (newUnif (), loc)
 388
 389                 val tf = checkExp G func
 390                 val ta = checkExp G arg
 391             in
 392                 (hasTyp (func, tf, (TArrow (dom, ran), loc));
 393                  hasTyp (arg, ta, dom)
 394                  handle Unify ue =>
 395                         dte (WrongType ("Function argument",
 396                                         arg,
 397                                         ta,
 398                                         dom,
 399                                         SOME ue));
 400                  ran)
 401                 handle Unify ue =>
 402                        (dte (WrongForm ("Function to be applied",
 403                                         "function",
 404                                         func,
 405                                         tf,
 406                                         SOME ue));
 407                         (TError, loc))
 408             end
 409
 410           | ESet (evar, e) =>
 411             let
 412                 val t = checkExp G e
 413             in
 414                 (TAction ((CPrefix (CRoot, loc), loc),
 415                           SM.empty,
 416                           SM.insert (SM.empty, evar, t)),
 417                  loc)
 418             end
 419           | EGet (x, evar, rest) =>
 420             let
 421                 val xt = (newUnif (), loc)
 422                 val G' = bindVal G (x, xt, NONE)
 423
 424                 val rt = whnorm (checkExp G' rest)
 425             in
 426                 case rt of
 427                     (TAction (p, d, r), _) =>
 428                     (case SM.find (d, evar) of
 429                          NONE => (TAction (p, SM.insert (d, evar, xt), r), loc)
 430                        | SOME xt' =>
 431                          (subTyp (xt', xt)
 432                                 handle Unify ue =>
 433                                        dte (WrongType ("Retrieved environment variable",
 434                                                        (EVar x, loc),
 435                                                        xt',
 436                                                        xt,
 437                                                        SOME ue));
 438                           rt))
 439                   | (TError, _) => rt
 440                   | _ => (dte (WrongForm ("Body of environment variable read",
 441                                           "action",
 442                                           rest,
 443                                           rt,
 444                                           NONE));
 445                           (TError, loc))
 446             end
 447
 448           | ESeq [] => raise Fail "Empty ESeq"
 449           | ESeq [e1] => checkExp G e1
 450           | ESeq (e1 :: rest) =>
 451             let
 452                 val e2 = (ESeq rest, loc)
 453
 454                 val t1 = whnorm (checkExp G e1)
 455                 val t2 = whnorm (checkExp G e2)
 456             in
 457                 case t1 of
 458                     (TAction (p1, d1, r1), _) =>
 459                     (case t2 of
 460                          (TAction (p2, d2, r2), _) =>
 461                          let
 462                              val p' = predSimpl (CAnd (p1, p2), loc)
 463
 464                              val d' = SM.foldli (fn (name, t, d') =>
 465                                                     case SM.find (r1, name) of
 466                                                         NONE =>
 467                                                         (case SM.find (d', name) of
 468                                                              NONE => SM.insert (d', name, t)
 469                                                            | SOME t' =>
 470                                                              (subTyp (t, t')
 471                                                               handle Unify ue =>
 472                                                                      dte (WrongType ("Shared environment variable",
 473                                                                                      (EVar name, loc),
 474                                                                                      t,
 475                                                                                      t',
 476                                                                                      SOME ue));
 477                                                               d'))
 478                                                       | SOME t' =>
 479                                                         (subTyp (t, t')
 480                                                          handle Unify ue =>
 481                                                                 dte (WrongType ("Shared environment variable",
 482                                                                                 (EVar name, loc),
 483                                                                                 t,
 484                                                                                 t',
 485                                                                                 SOME ue));
 486                                                          d'))
 487                                                 d1 d2
 488
 489                              val r' = SM.foldli (fn (name, t, r') => SM.insert (r', name, t))
 490                                                 r1 r2
 491                          in
 492                              (TAction (p', d', r'), loc)
 493                          end
 494                        | (TError, _) => t2
 495                        | _ => (dte (WrongForm ("Action to be sequenced",
 496                                                "action",
 497                                                e2,
 498                                                t2,
 499                                                NONE));
 500                                (TError, loc)))
 501                   | (TError, _) => t1
 502                   | _ => (dte (WrongForm ("Action to be sequenced",
 503                                           "action",
 504                                           e1,
 505                                           t1,
 506                                           NONE));
 507                           (TError, loc))
 508             end
 509
 510           | ELocal (e1, e2) =>
 511             let
 512                 val t1 = whnorm (checkExp G e1)
 513                 val t2 = whnorm (checkExp G e2)
 514             in
 515                 case t1 of
 516                     (TAction (p1, d1, r1), _) =>
 517                     (case t2 of
 518                          (TAction (p2, d2, r2), _) =>
 519                          let
 520                              val p' = predSimpl (CAnd (p1, p2), loc)
 521
 522                              val d' = SM.foldli (fn (name, t, d') =>
 523                                                     case SM.find (r1, name) of
 524                                                         NONE =>
 525                                                         (case SM.find (d', name) of
 526                                                              NONE => SM.insert (d', name, t)
 527                                                            | SOME t' =>
 528                                                              (subTyp (t, t')
 529                                                               handle Unify ue =>
 530                                                                      dte (WrongType ("Shared environment variable",
 531                                                                                      (EVar name, loc),
 532                                                                                      t,
 533                                                                                      t',
 534                                                                                      SOME ue));
 535                                                               d'))
 536                                                       | SOME t' =>
 537                                                         (subTyp (t, t')
 538                                                          handle Unify ue =>
 539                                                                 dte (WrongType ("Shared environment variable",
 540                                                                                 (EVar name, loc),
 541                                                                                 t,
 542                                                                                 t',
 543                                                                                 SOME ue));
 544                                                          d'))
 545                                                 d1 d2
 546                          in
 547                              (TAction (p', d', r2), loc)
 548                          end
 549                        | (TError, _) => t2
 550                        | _ => (dte (WrongForm ("Action to be sequenced",
 551                                                "action",
 552                                                e2,
 553                                                t2,
 554                                                NONE));
 555                                (TError, loc)))
 556                   | (TError, _) => t1
 557                   | _ => (dte (WrongForm ("Action to be sequenced",
 558                                           "action",
 559                                           e1,
 560                                           t1,
 561                                           NONE));
 562                           (TError, loc))
 563             end
 564
 565
 566           | EWith (e1, e2) =>
 567             let
 568                 val t1 = whnorm (checkExp G e1)
 569                 val t2 = whnorm (checkExp G e2)
 570             in
 571                 case t1 of
 572                     (TNested (pd, (TAction (pr, d1, r1), _)), _) =>
 573                     (case t2 of
 574                          (TAction (p, d, r), _) =>
 575                          if predImplies (pd, p) then
 576                              let
 577                                  val combineRecs =
 578                                      SM.unionWithi (fn (name, t1, t2) =>
 579                                                        (subTyp (t1, t2)
 580                                                         handle Unify ue =>
 581                                                                dte (WrongType ("Environment variable",
 582                                                                                (EVar name, loc),
 583                                                                                t1,
 584                                                                                t2,
 585                                                                                SOME ue));
 586                                                         t2))
 587                              in
 588                                  (TAction (pr, combineRecs (d, d1),
 589                                            combineRecs (r, r1)), loc)
 590                              end
 591                          else
 592                              (dte (WrongPred ("nested action",
 593                                               pd,
 594                                               p));
 595                               (TError, loc))
 596                        | (TError, _) => t2
 597                        | _ =>
 598                          (dte (WrongForm ("Body of nested action",
 599                                           "action",
 600                                           e2,
 601                                           t2,
 602                                           NONE));
 603                           (TError, loc)))
 604                   | (TError, _) => t1
 605                   | _ =>
 606                     (dte (WrongForm ("Container of nested action",
 607                                      "action",
 608                                      e1,
 609                                      t1,
 610                                      NONE));
 611                      (TError, loc))
 612             end
 613
 614           | ESkip => (TAction ((CPrefix (CRoot, loc), loc),
 615                                SM.empty, SM.empty), loc)
 616     end
 617
 618 exception Ununif
 619
 620 fun ununif (tAll as (t, loc)) =
 621     case t of
 622         TBase _ => tAll
 623       | TList t => (TList (ununif t), loc)
 624       | TArrow (d, r) => (TArrow (ununif d, ununif r), loc)
 625       | TAction (p, d, r) => (TAction (p, SM.map ununif d, SM.map ununif r), loc)
 626       | TUnif (_, ref (SOME t)) => ununif t
 627       | TNested _ => tAll
 628       | TError => tAll
 629
 630       | TUnif (_, ref NONE) => raise Ununif
 631
 632 fun hasError (t, _) =
 633     case t of
 634         TBase _ => false
 635       | TList t => hasError t
 636       | TArrow (d, r) => hasError d orelse hasError r
 637       | TAction (p, d, r) => List.exists hasError (SM.listItems d)
 638                              orelse List.exists hasError (SM.listItems r)
 639       | TNested _ => false
 640       | TError => false
 641       | TUnif (_, ref (SOME t)) => hasError t
 642       | TUnif (_, ref NONE) => false
 643
 644
 645 fun checkUnit G (eAll as (_, loc)) =
 646     let
 647         val _ = resetUnif ()
 648         val t = checkExp G eAll
 649     in
 650         if hasError t then
 651             t
 652         else
 653             ununif t
 654             handle Ununif =>
 655                    (ErrorMsg.error (SOME loc) "Unification variables remain in type:";
 656                     printd (p_typ t);
 657                     t)
 658     end
 659
 660 fun checkDecl G (d, _, loc) =
 661     case d of
 662         DExternType name => bindType G name
 663       | DExternVal (name, t) => bindVal G (name, checkTyp G t, NONE)
 664       | DVal (name, to, e) =>
 665         let
 666             val to =
 667                 case to of
 668                     NONE => (newUnif (), loc)
 669                   | SOME to => checkTyp G to
 670
 671             val t = checkExp G e
 672         in
 673             hasTyp (e, t, to)
 674             handle Unify ue =>
 675                    describe_type_error loc
 676                                        (WrongType ("Bound value",
 677                                                    e,
 678                                                    t,
 679                                                    to,
 680                                                    SOME ue));
 681             bindVal G (name, to, SOME e)
 682         end
 683       | DContext name => bindContext G name
 684
 685 fun checkFile G tInit (_, ds, eo) =
 686     let
 687         val G' = foldl (fn (d, G) => checkDecl G d) G ds
 688     in
 689         case eo of
 690             NONE => ()
 691           | SOME (e as (_, loc)) =>
 692             let
 693                 val t = checkExp G' e
 694             in
 695                 hasTyp (e, t, tInit)
 696                 handle Unify ue =>
 697                        (ErrorMsg.error (SOME loc) "Bad type for final expression of source file.";
 698                         preface ("Actual:", p_typ t);
 699                         preface ("Needed:", p_typ tInit))
 700             end;
 701         G'
 702     end
 703
 704 end