diff --git a/tests/issues/issue1024.icry b/tests/issues/issue1024.icry new file mode 100644 index 000000000..8d4b57876 --- /dev/null +++ b/tests/issues/issue1024.icry @@ -0,0 +1,4 @@ +:l issue1024a.cry +:l issue1024b.cry + +someFunc`{[16]} diff --git a/tests/issues/issue1024.icry.stdout b/tests/issues/issue1024.icry.stdout new file mode 100644 index 000000000..3eb547a3a --- /dev/null +++ b/tests/issues/issue1024.icry.stdout @@ -0,0 +1,27 @@ +Loading module Cryptol +Loading module Cryptol +Loading module Main +[warning] at issue1024a.cry:1:12--1:24 Unused name: f +[warning] at issue1024a.cry:2:14--2:24 Unused name: f +[warning] at issue1024a.cry:4:15--4:20 Unused name: i +[warning] at issue1024a.cry:4:22--4:32 Unused name: f +[warning] at issue1024a.cry:4:34--4:39 Unused name: g + +[error] at issue1024a.cry:1:6--1:11: + Illegal kind assigned to type variable: f`767 + Unexpected: # -> * + where + f`767 is signature variable 'f' at issue1024a.cry:1:12--1:24 +[error] at issue1024a.cry:2:6--2:13: + Illegal kind assigned to type variable: f`768 + Unexpected: Prop + where + f`768 is signature variable 'f' at issue1024a.cry:2:14--2:24 +[error] at issue1024a.cry:4:13--4:49: + Illegal kind assigned to type variable: f`770 + Unexpected: # -> * + where + f`770 is signature variable 'f' at issue1024a.cry:4:22--4:32 +Loading module Cryptol +Loading module Main +0xffff diff --git a/tests/issues/issue1024a.cry b/tests/issues/issue1024a.cry new file mode 100644 index 000000000..6ea2661dc --- /dev/null +++ b/tests/issues/issue1024a.cry @@ -0,0 +1,5 @@ +type Funny (f : # -> *) = Integer +type Strange (f : Prop) = Integer + +funnyFunc : { i : #, f : # -> *, g : * } Integer +funnyFunc = zero diff --git a/tests/issues/issue1024b.cry b/tests/issues/issue1024b.cry new file mode 100644 index 000000000..2a58a14eb --- /dev/null +++ b/tests/issues/issue1024b.cry @@ -0,0 +1,5 @@ + +type constraint PredSyn (a : *) (p:Prop) = (Zero a, Cmp a, p) + +someFunc : {a} (PredSyn a (Logic a)) => a +someFunc = ~zero