Блог

Главная - Вопросы по программированию - Компилятор Idris2 неожиданно пытается унифицировать значения типов

Компилятор Idris2 неожиданно пытается унифицировать значения типов

#idris

Вопрос:

Я столкнулся с ошибкой компиляции в Idris2, которую не могу объяснить, экспериментируя с монадами состояния Хоара:

 data PostS : (valType : Type) -> (stateType : Type) -> (valType -> stateType -> Type) -> Type where
  MkPostS
    :  (val : valType)
    -> (outState : stateType)
    -> {auto 0 prf : prop val outState}
    -> PostS valType stateType prop


mkPost : Nat -> PostS Nat Nat Equal
mkPost s2 = MkPostS s2 s2

f : (s1 : Nat) -> {auto 0 prf : Equal 0 s1} -> PostS Nat Nat (Equal)
f inState {prf} = MkPostS 7 7

компилятор жалуется , что он не может унифицировать inState и 7 в правой части f , что действительно не должно быть в состоянии сделать, но я бы тоже не ожидал, что он попытается.

Странная часть заключается в том, что замена правой части f на с mkPost 7 компилируется без ошибок, как и при использовании аналогичной лямбда-функции. Я в недоумении по поводу того, что здесь происходит.

ПРАВКА: еще несколько экспериментов

как отмечает @joel

 f : PostS Nat Nat (Equal)
f = MkPostS 7 7

Также терпит неудачу, пытаясь объединить 7 и 0, аналогично, определяя

 seven : Nat
seven = 7

имеет тот же результат, но:

 f' : (s1 : Nat) -> PostS Nat Nat (n => Equal (s1   n))
f' s1 = MkPostS 7 (s1 7)

работает. Это изначально заставило меня поверить , что это проблема, связанная с неоднозначностью типа 7 , но нет:

 data Foo = Bar | Baz

f'' : PostS Foo Foo (Equal)
f'' = MkPostS Baz Baz

Работает, объединяется Baz с Baz и пытается объединить Bar и Baz терпит неудачу , как и ожидалось, но MkPostS Bar Bar приводит к «Несоответствию между: База и бар», которое также исчезает при указании {prf=Refl} .

Я начинаю верить, что в компиляторе/проверке типов есть ошибка.

Комментарии:

1. любопытно, что если я удалю s1 параметр из f , я получу «Несоответствие между: 0 и 7».

2. он компилируется, если я добавлю {prf=Refl} MkPostS в f , но я бы ожидал, что Идрис сделает вывод, что

3. Ах, да, MyHoareMonad действительно не нужен, только что понял это сам. Отредактирует сообщение.

Метки: