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.

Sign up for GitHub

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

Jump to bottom

Reduced support for type classes in the inference of the return type of a match #13216

Closed
herbelin opened this issue Oct 17, 2020 · 0 comments · Fixed by #13217
Closed

Reduced support for type classes in the inference of the return type of a match #13216

herbelin opened this issue Oct 17, 2020 · 0 comments · Fixed by #13217
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: elaboration The elaboration engine, also known as the pretyper. part: typeclasses The typeclass mechanism.
Milestone
8.13+beta1

Comments

@herbelin
Copy link
Member

Description of the problem

While porting the containers contrib, I found this change of behavior which (a priori??) is not deliberate:

Class A.
Declare Instance a:A.
Inductive T `(A) := C.
Fail Definition f x := match x with C _ => 0 end.
(* Cannot infer the 1st argument of the inductive type (T) of this term (no type
class instance found). *)

Coq Version

Since commit fb1c2a0 (in version 8.10).
@herbelin herbelin added part: typeclasses The typeclass mechanism. part: elaboration The elaboration engine, also known as the pretyper. kind: bug An error, flaw, fault or unintended behaviour. labels Oct 17, 2020
@herbelin herbelin added this to the 8.13+beta1 milestone Oct 17, 2020
@herbelin herbelin mentioned this issue Oct 17, 2020
Merged
2 tasks
herbelin added a commit to herbelin/github-coq that referenced this issue Oct 25, 2020
@herbelin
Fixes coq#13216 (use of type classes in the return clause of a match).
bedc570 
This was deactivated in fb1c2a0 but it seems useful (e.g. in
contribs containers).

It seems to be useful
herbelin added a commit to herbelin/github-coq that referenced this issue Oct 26, 2020
@herbelin
Fixes coq#13216 (use of type classes in the return clause of a match).
f55aedf 
This was deactivated in fb1c2a0 but it seems useful (e.g. in
contribs containers).

It seems to be useful
herbelin added a commit to herbelin/github-coq that referenced this issue Oct 29, 2020
@herbelin
Fixes coq#13216 (use of type classes in the return clause of a match).
0ea1171 
This was deactivated in fb1c2a0 but it seems useful (e.g. in
contribs containers).

It seems to be useful
@ppedrot ppedrot closed this as completed in a9745d9 Nov 9, 2020
ppedrot added a commit that referenced this issue Nov 9, 2020
@ppedrot
Merge PR #13217: Addresses #13216: use of type classes in the return …
07472bc 
…clause of a match.

Reviewed-by: ppedrot
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug An error, flaw, fault or unintended behaviour. part: elaboration The elaboration engine, also known as the pretyper. part: typeclasses The typeclass mechanism.
Projects
None yet
Milestone
8.13+beta1
Development

Successfully merging a pull request may close this issue.

Addresses #13216: use of type classes in the return clause of a match. herbelin/github-coq
1 participant
@herbelin