[Agda] Error in pattern matching dependent family

[James Wood]

Hi Pierre,

This happens because, as far as the unifier is concerned, f need not be
injective. So there's not really anything that can be done about x and
y. Generalisation is the only way out.

If you want a practical way out, you probably should use rewrite.

  test : (X : Set) (x y : X) → (f : X → X) → (f x == f y) → (f y == f x)
  test X x y f eq rewrite eq = IDP

The documentation explains it, but it basically automates the with
abstraction you want to do.

Best wishes,

James

On 13/02/2019 21:45, Pierre Hyvernat wrote:
> Hello...
> 
> I've run into a new (for me) error while working with equality:
> Agda complains that
> 
> "I'm not sure if there should be a case for the constructor ..."
> 
> Here is a minimal file illustrating my problem:
> 
> ===== 8< =====
> module test where
> 
> -- the same happens with the builtin equality
> data _==_ {A : Set} (a : A) : A → Set where
>  IDP : a == a
> 
> test : (X : Set) (x y : X) → (f : X → X) → (f x == f y) → (f y == f x)
> test X x y f IDP = IDP
> 
> -- test : (X : Set) (x : X) → (f : X → X) → (f x == x) → (x == f x)
> -- test X x f IDP = IDP
> 
> ==============
> 
> The whole error message is
>   I'm not sure if there should be a case for the constructor IDP,
>   because I get stuck when trying to solve the following unification
>   problems (inferred index ≟ expected index):
>     f x ≟ f y
>   when checking that the pattern IDP has type f x == f y
> 
> I know I can prove this by generalizing and proving symmetry of _==_, or
> by defining and using the J eliminator for _==_.
> But is possible to do that directly with pattern matching? The error
> message isn't very helpful.
> 
> In my case, the output type (here "f y == f x") is quite big, and there
> are many more arguments with many dependencies. Generalizing is
> something I'd like to avoid...
> 
> 
> If that matters, in my case, it actually happens when trying to write a
> definition like
> 
>    test f x with previous-function (f x)
>    test f x | refl = ...
> 
> 
> Pierre

-- 
James Wood,
Department of Computer and Information Sciences,
University of Strathclyde.
The University of Strathclyde is a charitable body, registered in
Scotland, with registration number SC015263.