Inconsistent constraints leading to violated invariants in conversion checking

[GoogleCodeExporter]

{-# OPTIONS --allow-unsolved-metas #-}

module Bug where

record _×_ (A B : Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

app : {A B C : Set} → (A → B) × A → B
app (f , x) = f x

postulate
  P   : {A : Set} → A → Set
  p   : {A B C : Set} (f : A → B → C) {y : A} {v : B} → P y → P (f y v)
  A   : Set
  foo : (F : Set → Set) → (A → F A) → F A
  bar : (F : Set → Set) (f : A → F A) → P (foo F f)

q : P (app (foo (λ _ → (A → A) × A) (λ x → (λ x → x) , x)))
q = p (λ f x → app (f , x)) (bar ? ?)

-- An internal error has occurred. Please report this as a bug.
-- Location of the error: src/full/Agda/TypeChecking/Conversion.hs:668

The error above is raised by Agda 2.4.2, as well as the current
maintenance and master branch versions. Agda 2.3.2.2 accepts the file.

Original issue reported on code.google.com by nils.anders.danielsson on 24 Mar 2015 at 7:34

[vlopezj]

This is fine

@UlfNorell Or is it? When _23 is uninstantiated, the term foo (apply _23) (apply d) is ill-typed.

If I run agda --ignore-interfaces Issue1467.agda --verbose "tc.check.app:20" --verbose "tc.constr.add:80" --show-implicit --show-irrelevant --show-identity-substitutions --verbose "tc.meta.assign:20" --verbose "tc.conv:elim:25", one can find other ill-typed constraints, such as:

compareElims
  a     = _28 → Set
  pols0 (truncated to 10) =
  fors0 (truncated to 10) =
  v     = P {_28}
  els01 = [$ foo _24]
  els02 = [$ _26]

Perhaps I'm being too strict with what well-typed is in the context of Agda :)
I am looking a this in the context of implementing heterogeneous unification for Elims.

[vlopezj]

P.S.: I am thinking that having mismatched projection and elimination is not impossible in principle; one could have the following (well-typed, homogeneous) constraint:

a : A
b : B
p : (b : Bool) → if b then (A → B) else (A × B)

p true a =?= p false .snd : B

Although perhaps one can conjecture that, if the first arguments ("true" and "false") are reducible enough to affect whether the codomain is a function or a pair (A → B or A × B), then they are also reducible enough that they can be immediately deemed unequal, before reaching the point of checking "a" vs ".snd".