Skip to content

Commit

Permalink
Test case for issue #1024
Browse files Browse the repository at this point in the history
  • Loading branch information
robdockins committed Feb 11, 2021
1 parent 2f8ea90 commit fcfe0f8
Show file tree
Hide file tree
Showing 4 changed files with 41 additions and 0 deletions.
4 changes: 4 additions & 0 deletions tests/issues/issue1024.icry
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
:l issue1024a.cry
:l issue1024b.cry

someFunc`{[16]}
27 changes: 27 additions & 0 deletions tests/issues/issue1024.icry.stdout
Original file line number Diff line number Diff line change
@@ -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
5 changes: 5 additions & 0 deletions tests/issues/issue1024a.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
type Funny (f : # -> *) = Integer
type Strange (f : Prop) = Integer

funnyFunc : { i : #, f : # -> *, g : * } Integer
funnyFunc = zero
5 changes: 5 additions & 0 deletions tests/issues/issue1024b.cry
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@

type constraint PredSyn (a : *) (p:Prop) = (Zero a, Cmp a, p)

someFunc : {a} (PredSyn a (Logic a)) => a
someFunc = ~zero

0 comments on commit fcfe0f8

Please sign in to comment.