Idris - preuve à l'étape

Question

inductive Considérons la fonction suivante

tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber) 
tryMove Z from to [] = Nothing 
tryMove (S k) from to (smallestDiskPosition :: restOfTheDisposition) = 
     map (smallestDiskPosition ::) (tryMove k from to restOfTheDisposition) 

Essayer de compiler je reçois l'erreur suivante:

When checking argument prf to Hanoi.tryMove: 
     Type mismatch between 
       So True (Type of Oh) 
     and 
       So (from /= to) (Expected type) 

     Specifically: 
       Type mismatch between 
         True 
       and 
         not (Hanoi.Peg implementation of Prelude.Interfaces.Eq, method == from to) 

sur l'invocation de recurvise de tryMove. Si je passe comme dans {prf} explicitement

tryMove : (diskNumber : Nat) -> (from: Peg) -> (to: Peg)-> {default Oh prf: So (from /= to)} -> Disposition diskNumber -> Maybe (Disposition diskNumber) 
tryMove Z from to [] = Nothing 
tryMove (S k) from to {prf} (smallestDiskPosition :: restOfTheDisposition) = 
     map (smallestDiskPosition ::) (tryMove k from to {prf} restOfTheDisposition) 

Il compile correctement.

Pourquoi est-ce que Idris ne peut pas détecter automatiquement la preuve dans l'étape inductive, alors qu'il est capable de le faire dans une invocation normale de la fonction?

EDIT:

ici est un point essentiel complet à utiliser: https://gist.github.com/marcosh/d51479ea08e8522560713fd1e5ca9624

Answer 1

Vous fournissez la valeur par défaut (Oh) pour prf, si Idris tente de passer Oh dans l'appel récursif. Oh est de type So True et Idris attend prf être de type So (from /= to), mais puisque vous ne Destruct to et from, Idris ne peut pas connaître la valeur de from /= to, c'est pourquoi vous voyez ce message d'erreur.

Vous pouvez modifier la signature pour qu'elle contienne {auto prf: So (from /= to)} ou supprimer complètement l'argument prf, car vous ne l'utilisez pas réellement, vous le transmettez simplement dans l'appel récursif sans aucune modification.