search

Lysxia / coq-ceres

Coq library for serialization to S-expressions
MIT License
18 stars 1 forks source link

Add instances for id type #25

Closed liyishuai closed 3 years ago

liyishuai commented 3 years ago

Follow up https://github.com/Lysxia/coq-ceres/issues/9#issuecomment-544309941

Lysxia commented 3 years ago

I'm not sure about this. Having id in types sounds a bit too specialized to upstream.

liyishuai commented 3 years ago

I'm redefining these instances every time I start a new mini project. Not worth a coq-ceres-id package because it doesn't involve two independent libraries. Consider merging for now, until it breaks some dependant?

Lysxia commented 3 years ago

My primary concern is id being universe monomorphic, or has it been generalized lately? I'll merge this if it is polymorphic, and instance resolution still works with the universe-polymorphic id in your examples.

Another issue is that I don't fully understand the behavior of instances on transparent definitions. IMO that's the kind of uncertainty which is worth guarding against with a bit of copy-pasting across projects so you can easily take it out if problems do arise.

liyishuai commented 3 years ago

Close here if coq/coq#13873 is accepted.

liyishuai commented 3 years ago

Closing for now, since I'm the only user who copy-pastes the instance. Worth reopening if someone else has the same problem.