在 agda 中通过参数和返回类型重载

Question

我正在尝试编写一个形式为f : (X + Y) -> (Z + T)where X, Y, Z, Tare types的函数，它+是 sum 类型的伪符号。的返回类型f将由上下文确定，即在伪 agda 中

postulate x : X

t : T
t = f x -- OK, since (f : X -> T) definition is used

制作这样的东西很容易（再次在伪 agda 中，我试图简洁明了）：

fromX : X -> X + Y
toT : Z x T -> T

t2 : T
t2 = toT (f (fromX x))

但这对于我想要完成的事情来说太吵了。我尝试滥用实例查找。这是我想要工作但不进行类型检查的最小代码：

module Agda2 where
  infix 21 _·_
  infix 19 _?_

  data _?_ {n} {S : Set n} (x : S) : S ? Set n where
    refl : x ? x

  sym : ? {n} {S : Set n} {x y : S} ? x ? y ? y ? x
  sym refl = refl

  euc : ? {n} {S : Set n} {x y z : S} ? (x ? y) ? (x ? z) ? (y ? z)
  euc refl refl = refl

  postulate A : Set

  postulate _·_ : A ? A ? A

  postulate associative : ? {a b c} ? (a · b) · c ? a · (b · c)

  data _?_+_ (A : Set) : Set ? Set ? Set where
    instance
      sum-type? : ? {B : Set} ? A ? A + B
      sum-type? : ? {B : Set} ? A ? B + A

  assoc : ? {E1 E2 : Set} {a b c d : A}
    {{_ : E1 ? ((a · b) · c ? d) + (a · (b · c) ? d)}}
    {{_ : E2 ? ((a · b) · c ? d) + (a · (b · c) ? d)}}
    ? E1 ? E2
  assoc {{sum-type?}} {{sum-type?}} eq = euc associative eq
  assoc {{sum-type?}} {{sum-type?}} eq = euc (sym associative) eq  
  assoc {{sum-type?}} {{sum-type?}} eq = eq
  assoc {{sum-type?}} {{sum-type?}} eq = eq

  tt : ? {a b c d} ? (a · b) · c ? d ? (a · (b · c) ? d)
  tt eq = assoc eq

这段代码的问题是 Agda 无法推断a, b, c, d（我猜，但我不确定）。我通过这样做来规避这个问题：

  -- Everything is the same upto this point

  data _,_,_,_ (a b c d : A) : Set where
    v4 : a , b , c , d

  assoc : ? {E1 E2 : Set} {a b c d : A}
    {{_ : E1 ? ((a · b) · c ? d) + (a · (b · c) ? d)}}
    {{_ : E2 ? ((a · b) · c ? d) + (a · (b · c) ? d)}}
    ? (a , b , c , d) ? E1 ? E2
  assoc {{sum-type?}} {{sum-type?}} _ eq = euc associative eq
  assoc {{sum-type?}} {{sum-type?}} _ eq = euc (sym associative) eq  
  assoc {{sum-type?}} {{sum-type?}} _ eq = eq
  assoc {{sum-type?}} {{sum-type?}} _ eq = eq

  tt : ? {a b c d} ? (a , b , c , d) ? (a · b) · c ? d ? (a · (b · c) ? d)
  tt p eq = assoc p eq

这是有效的，因为现在 agda 明确地将其a, b, c, d作为参数（同样，这是我的理解，但我对 agda 内部了解不多）。但不幸的是，这并不实用，因为现在每个定理都需要一个额外的参数，以便类型检查器可以推断出正确的类型。

我为什么要这样做？我想要完成什么？我正在尝试编写一个通用assoc函数，这样我就不必为了进行关联相等推理而拥有数十个assoc函数assocl, assoc2, assoc' ...。我想一个函数，可以证明双方a(bc)=ab(c)和ab(c)=a(bc)等...

我究竟做错了什么？我该如何解决这个问题？任何帮助表示赞赏。谢谢！