Idris - Expression does not typecheck при импорте из модуля

Question

У меня есть модуль Idris, который определяет определенный тип/предикат IsSet и функцию разрешимости isSet над ним. Он также определяет некоторые вспомогательные функции для вычисления этой функции разрешимости при проверке типа для получения доказательства IsSet.

Выражения, которые используют вспомогательную функцию, что typecheck правильно внутри модуля, но не тогда, когда я определяю их в другой файл и импортировать исходный модуль:

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"] 

setTest1 typechecks правильно, но setTest2 выдает следующее сообщение об ошибке:

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) 

Я использую Идрис 0.12

Answer 1

При проверке Test2.idr типа, типа проверка не знает определения (в отличие от только типа) isSet, поэтому он не может уменьшить подпись типа getYes, следовательно, это несоответствие типа. Чтобы это работало, вы должны public export функция isSet. Из-за правил видимости Идриса вы также должны иметь не менее public export тип IsSet, потому что isSet ссылается на его (в настоящее время не экспортированное) определение.

Это, вероятно, хорошая идея, так или иначе, хотя, так как без этого, даже не простой функции, как

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

в Test2.idr будет работать, так как этот модуль не знает определения, т.е. конструкторов данных, типа.