regression/type-check.sml

   1 (* This example is interesting because at the time of generalization of f, the
   2  * tyvar 'a is in scope, but does not appear in type types of any of the
   3  * variables in the environment (x's type has not yet been determined to be 'a).
   4  * Nevertheless, it is essential to not generalize 'a at g
   5  *)
   6 val 'a f = fn x =>
   7   let
   8      exception E of 'a
   9      fun g (E y) = y
  10        | g _ = raise Fail "bug"
  11   in
  12      E x
  13   end
  14
  15 (* This example is interesting because it binds a type variable at a scope where
  16  * the type variable does not appear in the type.  Nevertheless, it is essential
  17  * to keep the type variable there, because it occurs in an inner scope.
  18  *)
  19 fun 'a f () =
  20    let
  21       val x: 'a = raise Fail "bug"
  22    in
  23       ()
  24    end
  25
  26 (* This example shows that type variables can be rebound in nested datatype
  27  * declarations, unlike the situation for nested value declarations.
  28  *)
  29 val 'a x =
  30    fn () =>
  31    let
  32       datatype 'a t = T of 'a
  33    in
  34       ()
  35    end
  36
  37 (* This example verifies that datatype replication is allowed, even when the
  38  * right-hand side isn't a datatype.
  39  *)
  40 type 'a t = 'a * 'a
  41 datatype u = datatype t
  42 val _: int u = (13, 14);
  43
  44 (* The following examples demonstrate acceptable forms of type variable scoping.
  45  *)
  46 fun f (x: 'a) =
  47    let
  48       fun g (y: 'a) = y
  49    in
  50       ()
  51    end
  52
  53 fun f (x: 'a) =
  54    let
  55       fun 'b g (y: 'b) = y
  56    in
  57       ()
  58    end
  59
  60 fun 'a f (x: 'a) =
  61    let
  62       fun g (y: 'a) = y
  63    in
  64       ()
  65    end
  66
  67 fun 'a f (x: 'a) =
  68    let
  69       fun 'b g (y: 'b) = y
  70    in
  71       ()
  72    end
  73
  74 val 'a x =
  75    fn () =>
  76    let
  77       datatype 'a t = T of 'a
  78    in
  79       ()
  80    end
  81
  82 (* This example confirms that bools can be used as labels. *)
  83 val {false = x, ...} = {false = 13};