examples/bts/17184.mlw

   1
   2 (*
   3
   4
   5 Error message: This expression has type t <> 'a 'b, but is expected to have type t 'a1 'a2
   6
   7 Clone substitute every occurrence of the type by the logic version, while
   8 we expect to use the program version in add.
   9
  10 *)
  11
  12 module A
  13
  14   type t
  15
  16   val add t : unit
  17
  18 end
  19
  20 module B
  21
  22   type t = { ghost a : unit }
  23
  24   clone export A with type t = t
  25
  26 (* FIXME !
  27   let sub (x:t) : unit = A.add x
  28 *)
  29 end