Следующий код загружается без ошибок в Idris 1.3.2:
data Thing = Rope
total Size : Thing -> Type
Size Rope = Double
total size : (thing : Thing) -> (Size thing = Double)
size Rope = Refl
total mkSize : (thing : Thing) -> Double -> Size thing
mkSize thing d =
case size thing of
Refl impossible
Но я не понимаю, почему. Для size thing не представляется невозможным быть Refl, учитывая, что именно так определяется size. Когда я запускаю пример вызова mkSize, похоже, что он застревает, сокращаясь:
*Test> mkSize Rope 0.3
case Refl of
Refl => _ : Double
Если я попытаюсь ввести «правильный» код:
total mkSize : (thing : Thing) -> Double -> Size thing
mkSize thing d =
case size thing of
Refl => d
, тогда я получите ошибку этого типа, которая предполагает, что Idris застрял, уменьшив Size thing, хотя Refl должен предоставить доказательство того, что это Double:
When checking left hand side of Main.case block in mkSize at Test.idr:11:10-19:
Type mismatch between
Double = Double (Type of Refl)
and
Size thing = Double (Expected type)
Specifically:
Type mismatch between
Double
and
Size thing
(я отредактировал сообщения об ошибках и подсказки для удаления полные пути)
Чего мне не хватает? Можно ли написать общую функцию, которая вот так застрянет?