[Agda] Surprising type error in implementing decreasing lists

[Conor McBride]

Hi Alan

This appears to be a bug. Somehow, some under-general unification
is happening.

On 20 Jul 2010, at 02:46, Alan Jeffrey wrote:

> a type which implements decreasing lists over a type (X : ℕ →  
> Set):
>
> data List<? (X : ℕ → Set) (n : ℕ) : Bool → Set where
>  [] : List<? X n true
>  _∷_ : {m : ℕ} → (x : X m) → (List<? X m true) → (List<? X  
> n (m lt n))
>
> List< : (ℕ → Set) → ℕ → Set
> List< X n = List<? X n true
>
> where lt is the obvious comparison function on ℕ.  Now, if I try to  
> build some elements of type (List< A 3) where:
>
> data A : ℕ → Set where
>  a1 : A 1
>  a2 : A 2
>
> but if I try to infer:

Now try sticking in ? and see what it asks you for...

> as' : List< A 3
> as' = a2 ∷ ? ∷ ?

...and you'll find it has decided that the first ? : A 0

That is, if you constrain m lt 2 to be true, m is somehow 0.

I also tried

foo : (P : Bool -> Set) -> ({m : ℕ} -> A m -> P (m lt 2)) -> P true
foo P p = p ?

and as asked for an A 0.

If I were a betting man, I'd bet Agda is making some attempt to
guess which functions are injective, in order to invert them, and
has somehow guessed wrongly about the nature of _lt_.

What's not at all clear to me, however, is how your first example
did work. I suppose, if the constraint solver makes bad choices,
you can still get lucky if the constraints get handled in a
convenient order.

All the best

Conor




>
> then I get an error:
>
> suc 0 != zero of type ℕ
> when checking that the expression a1 has type A 0
>
> Note, this is an error, not just some unsolved metavariables, which  
> surprises me.
>
> Agda version 2.2.6 in case it makes a difference.
>
> Any ideas anyone?
>
> Alan.
> <Weird.agda>_______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda