Stream: Coq users

Topic: Error message says a type is incompatible with itself.

view this post on Zulip Ezra elias kilty Cooper (Apr 28 2023 at 15:07):

I'm trying to apply a custom induction principle. Perhaps I've got it wrong. But the error message is confusing:

Error: Cannot instantiate metavariable P of type "Term -> Type" with abstraction
"fun M : Term =>
 forall (T : Ty) (tyEnv : list Ty) (Vs : list Term),
 Typing tyEnv M T ->
 env_typing Vs tyEnv -> env_Reducible Vs tyEnv -> Reducible (subst_env 0 Vs M) T"
of incompatible type "Term -> Type".

It says Term -> Type is incompatible with Term -> Type. Is this to do with universes? I tried to enable printing universes but that did not actually add any universe annotations to the relevant types. Is there some other invisible annotation I can enable to debug this?

view this post on Zulip Ana de Almeida Borges (Apr 28 2023 at 15:36):

You can enable all (most?) invisible printing with Set Printing All

view this post on Zulip Gaëtan Gilbert (Apr 28 2023 at 15:40):

could be an issue with delayed constraints, after instantiating the meta I think it will check the delayed constraints and if they produce an error it may think the error is because of the instantiation and so print what you got

view this post on Zulip Ezra elias kilty Cooper (Apr 29 2023 at 02:03):

@Gaëtan Gilbert Do you know what I might look for among the constraints? Print Universes emits a lot of stuff but it's too much to peck at.

Last updated: Oct 04 2023 at 22:01 UTC