src/tycheck.sml

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