Problem with patching and names

[jonsterling]

Not sure what is going on here, but consider the following example:

def category : type :=
  sig
    def ob : type
    def hom : sig [s : ob, t : ob] → type
    def idn : (x : ob) → hom # [s := x, t := x]
    def seq : (f : hom) → (g : hom # [s := f.t]) → hom # [s := f.s, t := g.t]

    def seqL :
      (f : hom) → path {hom # [s := f.s, t := f.t]} {seq {idn {f.s}} f} f

    def seqR :
      (f : hom) → path {hom # [s := f.s, t := f.t]} {seq f {idn {f.t}}} f

    def seqA :
      (f : hom) (g : hom # [s := f.t]) (h : hom # [s := g.t])
      → path {hom # [s := f.s, t := h.t]} {seq f {seq g h}} {seq {seq f g} h}
  end

def functor : type :=
  sig
    def s : category
    def t : category
    def ob : {s.ob} → {t.ob}
    def hom : (f : s.hom) → {t.hom # [s := ob {f.s}, t := ob {f.t}]}
    def idn : (x : s.ob) → path {t.hom # [s := ob x, t := ob x]} {hom {s.idn x}} {t.idn {ob x}}
    def seq : (f : s.hom) (g : s.hom # [s := f.t]) → path {t.hom # [s := ob {f.s}, t := ob {g.t}]} {hom {s.seq f g}} {t.seq {hom f} {hom g}}
  end

def nat-trans : type :=
  sig
    def src : functor
    def trg : functor # [s := src.s, t := src.t]
    def fam : (i : src.s.ob) → {src.t.hom # [s := src.ob i, t := trg.ob i]}

    def natural
      : (f : src.s.hom)
      → path {src.t.hom # [s := src.ob {f.s}, t := trg.ob {f.t}]}
          {src.t.seq {fam {f.s}} {trg.hom f}}
          {src.t.seq {src.hom f} {fam {f.t}}}
  end

In nat-trans, if I rename src,trg to s,t as I would like to, then the following happens:

[stdin]:34.38-34.41 [Error]:
  Expected (s₁ : sig 
  (ob : type)
  (hom : (_x₁ : sig def s : ob def t : ob end) → type)
  (idn : (x : ob) →
           sig
             def s : ext ob ⊤ {_x₁ => x}
             def t : ext ob ⊤ {_x₁ => x}
             def fib : hom {struct def s := x def t := x end}
           end)
  (seq : (f : sig def s : ob def t : ob def fib : hom {struct def s := s₂ def t := t end} end) →
           (g : sig
                  def s : ext ob ⊤ {_x₁ => f.t}
                  def t : ob
                  def fib : hom {struct def s := f.t def t := t end}
                end) →
             sig
               def s : ext ob ⊤ {_x₁ => f.s}
               def t : ext ob ⊤ {_x₁ => g.t}
               def fib : hom {struct def s := f.s def t := g.t end}
             end)
  (seqL : (f : sig def s : ob def t : ob def fib : hom {struct def s := s₂ def t := t end} end) →
            ext
              {i =>
                 sig
                   def s : ext ob ⊤ {_x₁ => f.s}
                   def t : ext ob ⊤ {_x₁ => f.t}
                   def fib : hom {struct def s := f.s def t := f.t end}
                 end}
              {i => i = 0 ∨ i = 1}
              {i _x₁ =>
                 [ i = 0 =>
                   struct
                     def s := f.s
                     def t := f.t
                     def fib :=
                       seq {struct
                              def s := idn {f.s}.s def t := idn {f.s}.t def fib := idn {f.s}.fib
                            end} {struct def s := f.s def t := f.t def fib := f.fib end}.fib
                   end
                 | i = 1 => struct def s := f.s def t := f.t def fib := f.fib end
                 ]})
  (seqR : (f : sig def s : ob def t : ob def fib : hom {struct def s := s₂ def t := t end} end) →
            ext
              {i =>
                 sig
                   def s : ext ob ⊤ {_x₁ => f.s}
                   def t : ext ob ⊤ {_x₁ => f.t}
                   def fib : hom {struct def s := f.s def t := f.t end}
                 end}
              {i => i = 0 ∨ i = 1}
              {i _x₁ =>
                 [ i = 0 =>
                   struct
                     def s := f.s
                     def t := f.t
                     def fib :=
                       seq {struct def s := f.s def t := f.t def fib := f.fib end} {
                       struct
                         def s := idn {f.t}.s def t := idn {f.t}.t def fib := idn {f.t}.fib
                       end}.fib
                   end
                 | i = 1 => struct def s := f.s def t := f.t def fib := f.fib end
                 ]})def seqA :
                      (f : sig
                             def s : ob def t : ob def fib : hom {struct def s := s₂ def t := t end}
                           end) →
                        (g : sig
                               def s : ext ob ⊤ {_x₁ => f.t}
                               def t : ob
                               def fib : hom {struct def s := f.t def t := t end}
                             end) →
                          (h : sig
                                 def s : ext ob ⊤ {_x₁ => g.t}
                                 def t : ob
                                 def fib : hom {struct def s := g.t def t := t end}
                               end) →
                            ext
                              {i =>
                                 sig
                                   def s : ext ob ⊤ {_x₁ => f.s}
                                   def t : ext ob ⊤ {_x₁ => h.t}
                                   def fib : hom {struct def s := f.s def t := h.t end}
                                 end}
                              {i => i = 0 ∨ i = 1}
                              {i _x₁ =>
                                 [ i = 0 =>
                                   struct
                                     def s := f.s
                                     def t := h.t
                                     def fib :=
                                       seq {struct def s := f.s def t := f.t def fib := f.fib end} {
                                       struct
                                         def s :=
                                           seq {struct def s := g.s def t := g.t def fib := g.fib end} {
                                           struct
                                             def s := h.s def t := h.t def fib := h.fib
                                           end}.s
                                         def t :=
                                           seq {struct def s := g.s def t := g.t def fib := g.fib end} {
                                           struct
                                             def s := h.s def t := h.t def fib := h.fib
                                           end}.t
                                         def fib :=
                                           seq {struct def s := g.s def t := g.t def fib := g.fib end} {
                                           struct
                                             def s := h.s def t := h.t def fib := h.fib
                                           end}.fib
                                       end}.fib
                                   end
                                 | i = 1 =>
                                   struct
                                     def s := f.s
                                     def t := h.t
                                     def fib :=
                                       seq {struct
                                              def s :=
                                                seq {struct
                                                       def s := f.s def t := f.t def fib := f.fib
                                                     end} {struct
                                                             def s := g.s
                                                             def t := g.t
                                                             def fib := g.fib
                                                           end}.s
                                              def t :=
                                                seq {struct
                                                       def s := f.s def t := f.t def fib := f.fib
                                                     end} {struct
                                                             def s := g.s
                                                             def t := g.t
                                                             def fib := g.fib
                                                           end}.t
                                              def fib :=
                                                seq {struct
                                                       def s := f.s def t := f.t def fib := f.fib
                                                     end} {struct
                                                             def s := g.s
                                                             def t := g.t
                                                             def fib := g.fib
                                                           end}.fib
                                            end} {struct
                                                    def s := h.s def t := h.t def fib := h.fib
                                                  end}.fib
                                   end
                                 ]}) to have field t

cooltt: encountered one or more errors

I wonder if the scoping of patches is a bit different than I had expected?

[mmcqd]

Each patch has all the previous patches in scope. So sig [A : type, B : type] # [A := nat, B := A] is valid in the empty context. I don't know if this is strictly needed though.

[mmcqd]

Actually with the recent record PR, each patch has all the fields of the record that precede it in scope. so sig [A : type, B : type] # [B := A] is also valid.

[jonsterling]

I feel having the previous patches in scope is unexpected behavior from a user's point of view...