Stream: Coq devs & plugin devs

Topic: bidi vs coercions

view this post on Zulip Gaƫtan Gilbert (Jun 30 2021 at 10:56):

The error in menhirlib for my latest attempt at automatic bidirectionality is quite annoying
Essentially the code is fun x : {x : supertype & _} => (projT1 x) : subtype
without bidi the body is elaborated to @projT1 supertype _ x which is then coerced to subtype
with bidi we understand that if @projT1 ?A ?B ?X : subtype then ?A == subtype and we type x with unsatisfiable type constraint

Is there no choice other than weakening the bidi?

view this post on Zulip Matthieu Sozeau (Jun 30 2021 at 11:53):

We probably should only say that there must be a coercion c : ?A <= subtype here... which might or might not be the identity

Last updated: Oct 16 2021 at 02:03 UTC