[Agda] Surprising type error in implementing decreasing lists

[Alan Jeffrey]

Hi everyone,

I'm not sure what's going on here, am I missing something?  Here's 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

then as long as I explicitly give the type of [] I'm OK:

as : List< A 3
as = a2 ∷ a1 ∷ ([] {A})

but if I try to infer it:

as' : List< A 3
as' = a2 ∷ a1 ∷ []

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.
-------------- next part --------------
open import Data.Nat
open import Data.Bool

module Weird where

infixr 5 _∷_

_lt_ : ℕ → ℕ → Bool
_     lt zero  = false
zero  lt suc _ = true
suc x lt suc y = x lt y

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

data A : ℕ → Set where
  a1 : A 1
  a2 : A 2

as : List< A 3
as = a2 ∷ a1 ∷ ([] {A})

as' : List< A 3
as' = a2 ∷ a1 ∷ []