Идрис: Ошибка проверки типа из-за 'rewrite__impl' - PullRequest
Новая
       13

Идрис: Ошибка проверки типа из-за 'rewrite__impl'

0 голосов
/ 01 января 2019

Я новичок в Idris и пытаюсь написать функцию, которая принимает Vect n Type и возвращает {a : Vect n Type} -> type_1 -> ... -> type_n -> HVect (reverse a).У меня есть это, чтобы проверить тип до последнего рекурсивного шага, где он терпит неудачу из-за функции rewrite__impl, застрявшей в типе.Вот код на данный момент: 

total funcGenerator : (Vect n Type) -> Type -> Type
funcGenerator []      out = out
funcGenerator (x::xs) out = x -> funcGenerator xs out

-- Reverse first argument, append second argument to it
total pileOn : Vect n Type -> Vect k Type -> Vect (plus n k) Type
pileOn               []      y = y
pileOn {n=S len} {k} (x::xs) y = rewrite plusSuccRightSucc len k in
                                     pileOn xs (x::y)

fetchArgsReverse : {h : Vect m Type} -> (b : Vect n Type) -> 
                   HVect h -> funcGenerator (HVect (pileOn b h))
fetchArgsReverse               [x]     y = (\p => p::y)
fetchArgsReverse {n=S len} {m} (x::xs) y = (\p => fetchArgsReverse xs (p::y))

Проверка типов жалуется так: 

|
| fetchArgsReverse {n=S len} {m} (x::xs) y = (\p => fetchArgsReverse xs (p::y))
|                                            ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking right hand side of fetchArgsReverse with expected type
    funcGenerator (x::xs) (HVect (pileOn (x::xs) h))

Type mismatch between
    funcGenerator xs (HVect (pileOn xs (x::h)))
        (Type of fetchArgsReverse xs (p::y))
and
    funcGenerator xs 
        (HVect (rewrite__impl (\replaced => Vect replaced Type)
        (plusSuccRightSucc len m) (pileOn xs (x::h)))) 
        (Expected Type)

(я добавил пробел.)

Что мне делатьоб этом rewrite__impl в ожидаемом виде?Как мне решить эту проблему?Функция pileOn не работает без перезаписи.

...