20070606-4

Attach:Prelude.agda Attach:Bug-TypeCheck.agda

See the second file.

  -- instantiation 
  inst : forall { iota1 iota2 n } -> 
             Ty' {iota2} (Succ n) -> Ty n -> Fin (Succ n) -> Kind' {iota1} -> Ty n

  inst{Succ iota1}{Succ iota2} (i · vs) u j (kap@(mkKind' kaps))
    = doapps {iota1} 
              (i [ u / j ] (\ x -> x)) 
              (map (\ v -> (inst {Succ iota1} v u j kap)) vs)
              kaps

The following error is reported

  Bug-TypeCheck.agda:105,53-56
  j != iota1 of type Nat
  when checking that the expression kap has type Kind'

Something's fishy here, since j is of type Fin _ whereas iota1 is of type Nat.

The error disappears when removing the @-pattern:

  ...
             (map (\ v -> (inst {Succ iota1} v u j (mkKind' kaps))) vs)
  ...

My guess is: The de Bruijn indices of the @-substitute (mkKind' kaps) are not properly lifted when stepping under the \ v binder.

I pay Ulf a beer if I am wrong!

Ulf: Then a beer I shall have! :-) The problem was that the as-binding got the wrong context from the start. The context for the as-bindings wasn't properly adjusted for dot patterns.

Andreas: So you shall! On my next visit to Chalmers, or whenever we meet next!