search

tchajed / coq-record-update

Library to create Coq record update functions
MIT License
42 stars 16 forks source link

Parameter name influences ability to determine setters #2

Closed sethomsen closed 5 years ago

sethomsen commented 5 years ago

Description of the problem

It seems like the parameter names of a function influences the ability to find instances of setters for records. Specifically any function i make which takes an argument named 'r' cannot determine any setter instances.

Steps to reproduce

`Record X := mkX { A: nat;}.

Instance etaX : Settable _ := mkSettable (pure mkX <*> A).

Definition setA (r : nat) x := x[A := 32].`

It does not matter wetter or not the argument is actually used in the function body, or if it annotated with explicit types.

Observed behaviour

`Error: Unable to satisfy the following constraints: In environment: r : nat x : X

?Setter : "Setter A"`

Expected behaviour

setA is defined

tchajed commented 5 years ago

Thanks for the report! Fixed by getting a fresh name in SetInstance_t.