Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Drop var constraint not solved #47

Closed
zilinc opened this issue Dec 8, 2016 · 1 comment
Closed

Drop var constraint not solved #47

zilinc opened this issue Dec 8, 2016 · 1 comment

Comments

@zilinc
Copy link

zilinc commented Dec 8, 2016

To compile

type RbtConsumeF k v acc obsv = RbtElemAO k v acc obsv -> acc
type RbtCondF k v acc obsv = (RbtElemAO k v acc obsv)! -> Bool

rbtFTrue: all(k:< DS, v :<DS, acc, obsv). RbtCondF k v acc obsv
rbtFTrue _ = True

I got:

Leftover constraint!
Drop acc
   in the 1st alternative _
   in the definition at ("rbt.cogent" (line 91, column 1))
   for the function rbtFTrue
Leftover constraint!
Drop obsv
   in the 1st alternative _
   in the definition at ("rbt.cogent" (line 91, column 1))
   for the function rbtFTrue

I don't think it's the same bug as #29, as type arguments are applied while calling rbtFTrue.

@liamoc
Copy link
Collaborator

liamoc commented Dec 11, 2016

Can you post a full example? I tried to compile this file:

type RbtElemAO k v acc obsv
type RbtConsumeF k v acc obsv = RbtElemAO k v acc obsv -> acc
type RbtCondF k v acc obsv = (RbtElemAO k v acc obsv)! -> Bool

rbtFTrue: all(k:< DS, v :<DS, acc, obsv). RbtCondF k v acc obsv
rbtFTrue _ = True

And it worked fine.

liamoc added a commit to liamoc/cogent that referenced this issue Dec 11, 2016
zilinc pushed a commit that referenced this issue Dec 11, 2016
zilinc pushed a commit that referenced this issue Dec 12, 2016
zilinc pushed a commit that referenced this issue Dec 12, 2016
zilinc pushed a commit that referenced this issue Dec 12, 2016
zilinc pushed a commit that referenced this issue Dec 12, 2016
@zilinc zilinc closed this as completed Dec 12, 2016
zilinc pushed a commit that referenced this issue Jan 12, 2017
zilinc pushed a commit that referenced this issue Jan 12, 2017
zilinc pushed a commit that referenced this issue Jan 12, 2017
zilinc pushed a commit that referenced this issue Jan 12, 2017
zilinc pushed a commit that referenced this issue Jan 12, 2017
zilinc pushed a commit that referenced this issue Jan 11, 2018
zilinc pushed a commit that referenced this issue Jan 11, 2018
zilinc pushed a commit that referenced this issue Jan 11, 2018
zilinc pushed a commit that referenced this issue Jan 11, 2018
zilinc pushed a commit that referenced this issue Jan 11, 2018
zilinc pushed a commit that referenced this issue Jan 22, 2018
zilinc pushed a commit that referenced this issue Jan 22, 2018
zilinc pushed a commit that referenced this issue Jan 22, 2018
zilinc pushed a commit that referenced this issue Jan 22, 2018
zilinc pushed a commit that referenced this issue Jan 22, 2018
zilinc pushed a commit that referenced this issue Mar 6, 2018
zilinc pushed a commit that referenced this issue Mar 6, 2018
zilinc pushed a commit that referenced this issue Mar 6, 2018
zilinc pushed a commit that referenced this issue Mar 6, 2018
zilinc pushed a commit that referenced this issue Mar 6, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants