Странная ошибка компилятора: невозможно объединить ограничение с помощью restint1 - PullRequest
Новая
       29

Странная ошибка компилятора: невозможно объединить ограничение с помощью restint1

1 голос
/ 10 июля 2019

Я пытаюсь написать библиотеку в Идрисе для работы с категориями и функторами. Для моего случая использования каждый тип может быть категорией не более чем одним способом (и я хотел бы использовать перегрузку для id и .), поэтому использование интерфейса соответствует моим потребностям: 

infixr 9 .
interface CategoryI (o : Type) where
  data Hom : o -> o -> Type
  (.) : {a : o} -> {b : o} -> {c : o} -> Hom b c -> Hom a b -> Hom a c
  id  : (a : o) -> Hom a a

Однако для функторов мне нужен тип данных, а не интерфейс, поскольку между одними и теми же двумя категориями может быть несколько функторов. 

data Functor : Type -> Type -> Type where
  MkFunctor : (CategoryI s, CategoryI t) => 
       (f : s -> t)
    -> (Hom x y -> Hom (f x) (f y))
    -> Functor s t

Чтобы использовать это, я написал функции доступа: 

src : Functor s t -> Type
src (MkFunctor fo fm) = s 

tgt : Functor s t -> Type
tgt (MkFunctor fo fm) = t

f_obj : (CategoryI s, CategoryI t) => Functor s t -> (s -> t)
f_obj (MkFunctor fo fm) = fo

Но у меня проблемы со следующим: 

f_map : (CategoryI s, CategoryI t) => (f : Functor s t)
     -> (Hom x y -> Hom ((f_obj f) x) ((f_obj f) y))
f_map (MkFunctor fo fm) = fm

Компилятор жалуется: 

 When checking right hand side of f_map with expected type
         Hom x y -> Hom (f_obj (MkFunctor fo fm) x) (f_obj (MkFunctor fo fm) y)

 Type mismatch between
         Hom x y -> Hom (fo x) (fo y) (Type of fm x y)
 and
         Hom x y -> Hom (fo x) (fo y) (Expected type)

 Specifically:
         Type mismatch between
                 constraint1
         and
                 constraint

  1. Я даже не могу определить, на что здесь жалуется компилятор. Он как-то не может объединить два ограничения (какие?), Но ограничения для моего конструктора и для моей f_map функции одинаковы, поэтому я не вижу, в чем проблема.

  2. Как я могу решить эту проблему?

...