Компиляция Идриса завершается неудачно - PullRequest
Новая
       22

Компиляция Идриса завершается неудачно

0 голосов
/ 16 марта 2019

Я пытаюсь формализовать делимость неотрицательных целых чисел в Идрисе следующим образом: 

data Divide : NonNeg n -> NonNeg d -> Type where
    MkDiv : {nn: NonNeg n} ->
         {dd : NonNeg d} ->
         (t : Zahlen) ->
         {auto tt : NonNeg t} ->
         (prf : (mul t d) = n) ->
         Divide nn dd

Затем я пытаюсь реализовать функцию с этим типом 

diw : (nn: NonNeg n) -> Divide nn nn
diw nn = ?hole

И когда я делаю это так, nn я получаю этот код, который является недопустимым для компилятора 

diw : (nn: NonNeg n) -> Divide nn nn
    diw NNpos = ?hole_1
    diw NNzero = ?hole_2

и это сообщение 

When checking left hand side of diw:
When checking argument nn to DivMod.diw:
    Type mismatch between
            NonNeg (Zpos s) (Type of NNpos)
    and
            NonNeg n (Expected type)

    Specifically:
            Type mismatch between
                    Zpos s
            and
                    n

Почему компилятор не может сделать вывод, что n связан свойством NonNeg?
Что-то не так с моей формализацией (стиль кода тоже)?
Каким правилам следует следовать, когда я делаю какой-то аргумент явным или неявным?

Целые числа (Захлена) и неотрицательность формализуются следующим образом: 

data Zahlen = Zero | Zpos (Nt.Positive x) | Zneg (Nt.Positive x)

data NonNeg: Zahlen -> Type where
    NNpos: NonNeg (Zpos s)
    NNzero: NonNeg Zero
...