Попытка ввести неявный аргумент в область слева от определения в Idris приводит к ошибке «применяется к слишком многим аргументам»

Question

Функция applyRule должна извлечь неявный аргумент n, который используется в других аргументах, которые он получает, типа VVect.

data IVect : Vect n ix -> (ix -> Type) -> Type where -- n is here
  Nil  : IVect Nil b
  (::) : b i -> IVect is b -> IVect (i :: is) b

VVect : Vect n Nat -> Type -> Type -- also here
VVect is a = IVect is (flip Vect a)

-- just for completeness
data Expression = Sigma Nat Expression

applyRule : (signals : VVect is Double) ->
            (params : List Double) ->
            (sigmas : List Double) ->
            (rule : Expression) ->
            Double

applyRule {n} signals params sigmas (Sigma k expr1) = cast n

Без ссылки на {n},проверки типа кода (если cast n заменено на некоторое допустимое значение double).Однако его добавление приводит к следующей ошибке:

When checking left hand side of applyRule:
Type mismatch between
        Double (Type of applyRule signals params sigmas rule)
and
        _ -> _ (Is applyRule signals
                             params
                             sigmas
                             rule applied to too many arguments?)

Мне кажется, что это не имеет смысла, потому что я не сопоставляю шаблон с любым параметром, который может зависеть от n, поэтому я подумал, что простое вложение в фигурные скобки приведет его в область видимости.

Answer 1

Вы можете ввести n в область действия, только если она где-то определена (например, как переменная в аргументах).В противном случае было бы трудно понять, откуда взялся n - по крайней мере, для человека.

applyRule : {is : Vect n Nat} ->
            (signals : VVect is Double) ->
            (params : List Double) ->
            (sigmas : List Double) ->
            (rule : Expression) ->
            Double
applyRule {n} signals params sigmas (Sigma k expr1) = cast n