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".
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?
You can enable all (most?) invisible printing with
Set Printing All
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
@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