Функция X проходит проверку типа, а DependentMealy - нет.Мне кажется, что они оба одинаковы.Первый аргумент - это состояние.Второй аргумент - это функция, которая задает тип ввода для машины из текущего состояния.Третий аргумент - это функция, которая дает новое состояние.Четвертый аргумент - это функция, которая задает тип вывода мучного аппарата.Состояние подразумевается как уровень типа.
X : state -> (opt : state -> Type) -> ((s : state) -> opt s -> state) -> ((s : state) -> opt s -> Type) -> Type
X s f1 f2 f3 = (op : f1 s) -> (f3 s op, X (f2 s op) f1 f2 f3)
data DependentMealy : state -> (opt : state -> Type) -> ((s : state) -> opt s -> state) -> ((s : state) -> opt s -> Type) -> Type where
MkDependentMealy : ((op : f1 s) -> (f3 s op, DependentMealy (f2 s op) f1 f2 f3)) -> DependentMealy s f1 f2 f3
При проверке типа NewM.MkDependentMealy: при проверке приложения NewM.DependentMealy:
Несоответствие типов между
phTy -> f1 s -> Type (Type of f3)
и
(s8 : phTy) -> f1 s8 -> Type (Expected type)
В частности: Несоответствие типов между
f1 s
и
f1 v0