Gaëtan Gilbert (Jun 30 2021 at 10:56): 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?
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: Dec 05 2023 at 11:01 UTC