Idris - Expression doesnt typecheck beim Importieren von Modul

Question

Ich habe ein Idris-Modul, das einen bestimmten Typ/Prädikat IsSet und eine Entscheidungsfunktion isSet darüber definiert. Es definiert auch einige Hilfsfunktionen, um diese Decidability-Funktion bei der Typprüfung zu berechnen, um einen Beweis von IsSet zu erhalten.

Ausdrücke, die die Hilfsfunktion typecheck verwenden korrekt innerhalb des Moduls, aber nicht, wenn ich sie in einer anderen Datei definieren und ich importieren Sie die Original-Modul:

Test1.idr

module Test1 

import Data.List 

%default total 
%access export 

data IsSet : List t -> Type where 
    IsSetNil : IsSet [] 
    IsSetCons : Not (Elem x xs) -> IsSet xs -> IsSet (x :: xs) 

ifNotSetHereThenNeitherThere : Not (IsSet xs) -> Not (IsSet (x :: xs)) 
ifNotSetHereThenNeitherThere notXsIsSet (IsSetCons xIsInXs xsIsSet) = notXsIsSet xsIsSet 

ifIsElemThenConsIsNotSet : Elem x xs -> Not (IsSet (x :: xs))  
ifIsElemThenConsIsNotSet xIsInXs (IsSetCons notXIsInXs xsIsSet) = notXIsInXs xIsInXs 

isSet : DecEq t => (xs : List t) -> Dec (IsSet xs) 
isSet [] = Yes IsSetNil 
isSet (x :: xs) with (isSet xs) 
    isSet (x :: xs) | No notXsIsSet = No $ ifNotSetHereThenNeitherThere notXsIsSet 
    isSet (x :: xs) | Yes xsIsSet with (isElem x xs) 
    isSet (x :: xs) | Yes xsIsSet | No notXInXs = Yes $ IsSetCons notXInXs xsIsSet 
    isSet (x :: xs) | Yes xsIsSet | Yes xInXs = No $ ifIsElemThenConsIsNotSet xInXs 

getYes : (d : Dec p) -> case d of { No _ =>(); Yes _ => p} 
getYes (No _) =() 
getYes (Yes prf) = prf 

getNo : (d : Dec p) -> case d of { No _ => Not p; Yes _ =>()} 
getNo (No cnt) = cnt 
getNo (Yes _) =() 

setTest1 : IsSet ["x"] 
setTest1 = getYes $ isSet ["x"] 

Test2.idr

module Test2 

import Test1 

%default total 
%access export 

setTest2 : IsSet ["x"] 
setTest2 = getYes $ isSet ["x"] 

richtigtypechecks aber setTest2 führt den folgenden Fehler:

When checking right hand side of setTest2 with expected type 
     IsSet ["x"] 

Type mismatch between 
     case block in getYes at Test1.idr:26:30 (IsSet ["x"]) 
               (isSet ["x"]) 
               (isSet ["x"]) (Type of getYes (isSet ["x"])) 
and 
     IsSet ["x"] (Expected type) 

Ich bin mit Idris 0,12

Answer 1

Wenn Typ Test2.idr Überprüfung der Typprüfer nicht die Definition kennt (im Gegensatz zu nur die Art) von isSet, so kann es nicht die Typ-Signatur von getYes, daher der Typ nicht übereinstimmen. Damit dies funktioniert, müssen Sie public export die Funktion isSet. Aufgrund von Idris Sichtbarkeitsregeln müssen Sie dann auch mindestens public export den IsSet Typ angeben, da isSet auf seine (derzeit nicht exportierte) Definition verweist. Diese

ist wahrscheinlich eine gute Idee, wie auch immer, obwohl, da ohne dass nicht einmal eine einfache Funktion wie

isNil : IsSet l -> Bool 
isNil IsSetNil = True 
isNil (IsSetCons f y) = False 

in Test2.idr funktionieren würde, da das Modul die Definition nicht kennt, dh die Daten Bauer, vom Typ.