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 https://gitlab.com/SkySkimmer/coq/-/jobs/1385663691 https://gitlab.inria.fr/fpottier/menhir/-/blob/20210310/coq-menhirlib/src/Interpreter.v#L144 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