[Agda] More aggressive type reconstruction?

[Andreas Abel]

[I am putting this message here for the record, we can discuss it on  
the Agda meeting]

Currently, I am formalizing strongly typed System F terms.  I have a  
Coq formalization which I am porting to Agda since my Coq definitions  
did not give me the correct rewrites.  In the Agda code, I can write  
less "_" then in the Coq code.

It seems that Coq's type reconstruction is more aggressive.  E.g. I  
can write (details do not matter):

Lemma cxtSubst_shift_lift {n m} {Gamma : Cxt m} {sigma : TySubst n m} :
   cxtSubst (cxtShift1 Gamma) (tySubstLift sigma) = cxtShift1  
(cxtSubst Gamma sigma).

Fixpoint tmSubstTy {n m}{Gamma : Cxt m}{T dir any}
   (t : Tm Gamma T dir any) :
     forall (sigma : TySubst n m),
       Tm (cxtSubst Gamma sigma) (tySubst T sigma) dir any  :=
   match t in ... return ... with
     ...
   | tAbs  T  _ t    => fun sigma =>
      tAbs (eq_rec _ (fun G => Tm G _ _ _)
             (tmSubstTy t (tySubstLift sigma)) _ cxtSubst_shift_lift)
    ...
   end.

The point I want to make here is that when giving the predicate where  
substitution by eq_rec should happen, I can simply write

   (fun G => Tm G _ _ _)

The same function in Agda:

data Tm {n} (Γ : Cxt n) : Ty n → Dir → Norm → Set where
   ...
   tAbs : ∀ {T any} →
          Tm (shiftG Γ) T chk any →
          Tm Γ (tyAll T) chk any

_t○S_ : ∀ {m n} {Γ : Cxt m} {T : Ty m} {dir any} →
         Tm Γ T dir any → (σ : n ⊢S m) → Tm (Γ G○S σ) (T  
T○S σ) dir any

-- tAbs t   t○S σ = tAbs (t t○S liftS σ)
tAbs {T = T}{any = any} t  t○S σ =
   tAbs (subst (λ Γ → Tm Γ (T T○S liftS σ) chk any)
               shiftG○liftS
               (t t○S liftS σ))

For the first argument of subst, I tried (λ Γ → Tm Γ _ _ _) first  
as in Coq, but it fails, nothing short of the full term

   (λ Γ → Tm Γ (T T○S liftS σ) chk any)

works.  One would think one could make Agda type reconstruction  
stronger by adding some heuristics.  These would be "unsafe"  
reconstruction steps, probably.  But one could do unsafe steps after  
all safe steps have been done, if the alternative is to fail  
immediately.

Cheers,
Andreas

Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41