1(* test generation of signature mismatch errors *) 2 3(* misc tests --- not exhaustive *) 4 5structure X = struct open General end: sig val + : (int * int) -> int end; 6structure X = struct val x = fn 1 => Div end : sig exception x of int end; 7structure X = struct val x = fn y => y end : sig prim_val x : 'a ->'a = 1 "identity" end; 8exception e (* static *); 9structure X = struct exception e = e end : sig exception e (* dynamic *) end; 10structure X = struct val x = fn 1 => 1 end : sig val x : 'a -> 'a end; 11structure X = struct val x = fn 1 => Div end : sig exception x of int end; 12structure X = struct val x = fn y => y end : sig prim_val x : 'a ->'a = 1 "identity" end; 13structure X = struct datatype t = C of int end : sig datatype t = C of bool end; 14 15signature S = sig type t end where type 'a t = int; 16signature S = sig structure X : sig type t end end where type 'a X.t = int; 17signature S = sig structure Y : sig structure X : sig type t end end end where type 'a Y.X.t = int; 18 19(* module mismatches *) 20structure X = struct end:functor(X:sig end)->sig end; 21functor X = (functor(X:sig end)=>struct end) : sig end; 22functor X = (functor(X:sig end)=>struct end): functor(X:sig end)->functor(X:sig end)->sig end; 23functor X = (functor(X:sig end)=>functor(X:sig end)=>struct end): functor(X:sig end)->sig end; 24functor X = (functor(X:functor(X:sig end)->sig end)=>struct end): functor(X:sig end)->sig end; 25functor X = (functor(X:sig end)=>struct end): functor(F:functor(X:sig end)->sig end)->sig end; 26 27 28(* systematic tests *) 29 30(* missing type declarations *) 31 32signature G = sig type t = unit end; 33signature L = sig end; 34 35functor L = functor (L:L)=> 36 L:G; 37functor LL = functor(LL:functor(L:L)->L)=> 38 LL:functor(L:L)->G; 39functor GL = functor(GL:functor(L:G)->L)=> 40 GL:functor(L:L)->L; 41functor YL = functor(YL:sig structure Y:L end)=> 42 YL:sig structure Y: G end; 43functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 44 L_YL:functor(L:L)->sig structure Y: G end; 45functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 46 YG_L:functor(YL:sig structure Y: L end)->L; 47functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 48 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 49functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 50 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 51 52(* missing value declarations *) 53 54signature G = sig val x: unit end; 55signature L = sig end; 56 57functor L = functor (L:L)=> 58 L:G; 59functor LL = functor(LL:functor(L:L)->L)=> 60 LL:functor(L:L)->G; 61functor GL = functor(GL:functor(L:G)->L)=> 62 GL:functor(L:L)->L; 63functor YL = functor(YL:sig structure Y:L end)=> 64 YL:sig structure Y: G end; 65functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 66 L_YL:functor(L:L)->sig structure Y: G end; 67functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 68 YG_L:functor(YL:sig structure Y: L end)->L; 69functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 70 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 71functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 72 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 73 74(* missing structure declarations *) 75 76signature G = sig structure X: sig end end; 77signature L = sig end; 78 79functor L = functor (L:L)=> 80 L:G; 81functor LL = functor(LL:functor(L:L)->L)=> 82 LL:functor(L:L)->G; 83functor GL = functor(GL:functor(L:G)->L)=> 84 GL:functor(L:L)->L; 85functor YL = functor(YL:sig structure Y:L end)=> 86 YL:sig structure Y: G end; 87functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 88 L_YL:functor(L:L)->sig structure Y: G end; 89functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 90 YG_L:functor(YL:sig structure Y: L end)->L; 91functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 92 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 93functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 94 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 95 96(* missing functor declarations *) 97 98signature G = sig functor F:functor(X:sig end)->sig end 99 end; 100signature L = sig end; 101 102functor L = functor (L:L)=> 103 L:G; 104functor LL = functor(LL:functor(L:L)->L)=> 105 LL:functor(L:L)->G; 106functor GL = functor(GL:functor(L:G)->L)=> 107 GL:functor(L:L)->L; 108functor YL = functor(YL:sig structure Y:L end)=> 109 YL:sig structure Y: G end; 110functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 111 L_YL:functor(L:L)->sig structure Y: G end; 112functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 113 YG_L:functor(YL:sig structure Y: L end)->L; 114functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 115 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 116functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 117 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 118 119(* scheme mismatch *) 120 121signature G = sig val x : 'a -> 'a end; 122signature L = sig val x : int -> int end; 123 124functor L = functor (L:L)=> 125 L:G; 126functor LL = functor(LL:functor(L:L)->L)=> 127 LL:functor(L:L)->G; 128functor GL = functor(GL:functor(L:G)->L)=> 129 GL:functor(L:L)->L; 130functor YL = functor(YL:sig structure Y:L end)=> 131 YL:sig structure Y: G end; 132functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 133 L_YL:functor(L:L)->sig structure Y: G end; 134functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 135 YG_L:functor(YL:sig structure Y: L end)->L; 136functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 137 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 138functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 139 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 140 141(* scheme mismatch with free type parameter *) 142val 'b fail = 143let 144 signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end; 145 signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end; 146 147 functor L = functor (L:L)=> 148 L:G; 149in unit 150end 151; 152val 'b fail = 153let 154 signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end; 155 signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end; 156 functor LL = functor(LL:functor(L:L)->L)=> 157 LL:functor(L:L)->G; 158in unit 159end 160; 161val 'b fail = 162let 163 signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end; 164 signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end; 165 functor GL = functor(GL:functor(L:G)->L)=> 166 GL:functor(L:L)->L; 167in unit 168end 169; 170val 'b fail = 171let 172 signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end; 173 signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end; 174 functor YL = functor(YL:sig structure Y:L end)=> 175 YL:sig structure Y: G end; 176in unit 177end 178; 179val 'b fail = 180let 181 signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end; 182 signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end; 183 functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 184 L_YL:functor(L:L)->sig structure Y: G end; 185in unit 186end 187; 188val 'b fail = 189let 190 signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end; 191 signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end; 192 functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 193 YG_L:functor(YL:sig structure Y: L end)->L; 194in unit 195end 196; 197val 'b fail = 198let 199 signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end; 200 signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end; 201 functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 202 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 203in unit 204end 205; 206val 'b fail = 207let 208 signature L = sig val x : ('a -> 'a) -> ('b -> 'b) end; 209 signature G = sig val x : ('a -> 'a) -> ('a -> 'a) end; 210 functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 211 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 212in () 213end; 214 215(* status mismatch *) 216 217signature G = sig exception x end; 218signature L = sig val x : exn end; 219 220functor L = functor (L:L)=> 221 L:G; 222functor LL = functor(LL:functor(L:L)->L)=> 223 LL:functor(L:L)->G; 224functor GL = functor(GL:functor(L:G)->L)=> 225 GL:functor(L:L)->L; 226functor YL = functor(YL:sig structure Y:L end)=> 227 YL:sig structure Y: G end; 228functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 229 L_YL:functor(L:L)->sig structure Y: G end; 230functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 231 YG_L:functor(YL:sig structure Y: L end)->L; 232functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 233 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 234functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 235 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 236 237(* conenv mismatch *) 238 239signature G = sig datatype t = C of int end; 240signature L = sig datatype t = D of int end; 241 242functor L = functor (L:L)=> 243 L:G; 244functor LL = functor(LL:functor(L:L)->L)=> 245 LL:functor(L:L)->G; 246functor GL = functor(GL:functor(L:G)->L)=> 247 GL:functor(L:L)->L; 248functor YL = functor(YL:sig structure Y:L end)=> 249 YL:sig structure Y: G end; 250functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 251 L_YL:functor(L:L)->sig structure Y: G end; 252functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 253 YG_L:functor(YL:sig structure Y: L end)->L; 254functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 255 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 256functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 257 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 258 259(* arity mismatch *) 260 261signature G = sig type t = unit end; 262signature L = sig type 'a t = unit end; 263 264functor L = functor (L:L)=> 265 L:G; 266functor LL = functor(LL:functor(L:L)->L)=> 267 LL:functor(L:L)->G; 268functor GL = functor(GL:functor(L:G)->L)=> 269 GL:functor(L:L)->L; 270functor YL = functor(YL:sig structure Y:L end)=> 271 YL:sig structure Y: G end; 272functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 273 L_YL:functor(L:L)->sig structure Y: G end; 274functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 275 YG_L:functor(YL:sig structure Y: L end)->L; 276functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 277 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 278functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 279 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 280 281(* ref equality mismatch *) 282 283signature G = sig datatype myref = datatype ref end; 284signature L = sig type 'a myref = 'a end; 285 286functor L = functor (L:L)=> 287 L:G; 288functor LL = functor(LL:functor(L:L)->L)=> 289 LL:functor(L:L)->G; 290functor GL = functor(GL:functor(L:G)->L)=> 291 GL:functor(L:L)->L; 292functor YL = functor(YL:sig structure Y:L end)=> 293 YL:sig structure Y: G end; 294functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 295 L_YL:functor(L:L)->sig structure Y: G end; 296functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 297 YG_L:functor(YL:sig structure Y: L end)->L; 298functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 299 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 300functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 301 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 302 303(* ref equality mismatch *) 304 305signature G = sig prim_EQtype t end; 306signature L = sig type t end; 307 308functor L = functor (L:L)=> 309 L:G; 310functor LL = functor(LL:functor(L:L)->L)=> 311 LL:functor(L:L)->G; 312functor GL = functor(GL:functor(L:G)->L)=> 313 GL:functor(L:L)->L; 314functor YL = functor(YL:sig structure Y:L end)=> 315 YL:sig structure Y: G end; 316functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 317 L_YL:functor(L:L)->sig structure Y: G end; 318functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 319 YG_L:functor(YL:sig structure Y: L end)->L; 320functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 321 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 322functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 323 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 324 325(* equality mismatch *) 326 327signature G = sig eqtype t end; 328signature L = sig type t = unit -> unit end; 329 330functor L = functor (L:L)=> 331 L:G; 332functor LL = functor(LL:functor(L:L)->L)=> 333 LL:functor(L:L)->G; 334functor GL = functor(GL:functor(L:G)->L)=> 335 GL:functor(L:L)->L; 336functor YL = functor(YL:sig structure Y:L end)=> 337 YL:sig structure Y: G end; 338functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 339 L_YL:functor(L:L)->sig structure Y: G end; 340functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 341 YG_L:functor(YL:sig structure Y: L end)->L; 342functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 343 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 344functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 345 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 346 347(* transparent mismatch *) 348 349signature G = sig type t = unit end; 350signature L = sig type t = unit -> unit end; 351 352functor L = functor (L:L)=> 353 L:G; 354functor LL = functor(LL:functor(L:L)->L)=> 355 LL:functor(L:L)->G; 356functor GL = functor(GL:functor(L:G)->L)=> 357 GL:functor(L:L)->L; 358functor YL = functor(YL:sig structure Y:L end)=> 359 YL:sig structure Y: G end; 360functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 361 L_YL:functor(L:L)->sig structure Y: G end; 362functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 363 YG_L:functor(YL:sig structure Y: L end)->L; 364functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 365 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 366functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 367 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 368 369(* datatype mismatch *) 370 371signature G = sig datatype t = C end; 372signature L = sig type t = unit end; 373 374functor L = functor (L:L)=> 375 L:G; 376functor LL = functor(LL:functor(L:L)->L)=> 377 LL:functor(L:L)->G; 378functor GL = functor(GL:functor(L:G)->L)=> 379 GL:functor(L:L)->L; 380functor YL = functor(YL:sig structure Y:L end)=> 381 YL:sig structure Y: G end; 382functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 383 L_YL:functor(L:L)->sig structure Y: G end; 384functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 385 YG_L:functor(YL:sig structure Y: L end)->L; 386functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 387 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 388functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 389 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 390 391(* scope violations *) 392 393signature G = functor X:sig type t end ->sig type u end; 394signature L = functor(X:sig type t end)->sig type u end; 395 396functor L = functor (L:L)=> 397 L:G; 398functor LL = functor(LL:functor(L:L)->L)=> 399 LL:functor(L:L)->G; 400functor GL = functor(GL:functor(L:G)->L)=> 401 GL:functor(L:L)->L; 402 403(* scope violations (cont.) 404 we need to embed the functors in structures for these tests *) 405 406signature G = sig functor F: functor X:sig type t end ->sig type u end end; 407signature L = sig functor F: functor(X:sig type t end)->sig type u end end; 408 409functor YL = functor(YL:sig structure Y:L end)=> 410 YL:sig structure Y: G end; 411functor L_YL = functor(L_YL:functor(L:L)->sig structure Y:L end)=> 412 L_YL:functor(L:L)->sig structure Y: G end; 413functor YG_L = functor(YG_L:functor(YG:sig structure Y:G end)->L)=> 414 YG_L:functor(YL:sig structure Y: L end)->L; 415functor L_YG_L = functor(L_YG_L:functor(L:L)->functor(YG:sig structure Y:G end)->L)=> 416 L_YG_L:functor(L:L)->functor(YL:sig structure Y:L end)->L; 417functor FLYGL = functor(FLYGL:sig functor F: functor(L:L)->functor(YG:sig structure Y:G end)->L end)=> 418 FLYGL:sig functor F: functor(L:L)->functor(YL:sig structure Y:L end)->L end; 419 420 421 422 423 424 425 426 427 428