summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAlasdair2018-08-18 00:47:10 +0100
committerAlasdair2018-08-18 00:47:10 +0100
commit79176c7ac58900c95db5db9cf75978e91e9a453c (patch)
tree79a3f2d4db576fe594cf4e2c17db0b37217df6d7 /test
parentc0f68b6712c916a3cf16f933840a48ec22330289 (diff)
Correctly specialise type annotation in polymorphic functions
Diffstat (limited to 'test')
-rw-r--r--test/c/special_annot.expect1
-rw-r--r--test/c/special_annot.sail19
2 files changed, 20 insertions, 0 deletions
diff --git a/test/c/special_annot.expect b/test/c/special_annot.expect
new file mode 100644
index 00000000..ee8a39c3
--- /dev/null
+++ b/test/c/special_annot.expect
@@ -0,0 +1 @@
+string
diff --git a/test/c/special_annot.sail b/test/c/special_annot.sail
new file mode 100644
index 00000000..ca2f5f4c
--- /dev/null
+++ b/test/c/special_annot.sail
@@ -0,0 +1,19 @@
+
+union option ('a : Type) = {
+ None : unit,
+ Some : 'a
+}
+
+val test : forall ('a : Type). 'a -> option('a)
+
+function test(x) =
+ let y : 'a = x in Some(y)
+
+val "print_endline" : string -> unit
+
+val main : unit -> unit
+
+function main() = {
+ let Some(y) = test("string");
+ print_endline(y)
+} \ No newline at end of file