Идрис подразумевает сообщение об ошибке "... не является неявным аргументом ..." - PullRequest
Новая
       16

Идрис подразумевает сообщение об ошибке "... не является неявным аргументом ..."

1 голос
/ 15 марта 2019

У меня есть следующее определение интерфейса в файле A : 

interface Loader (c : Type -> Type) r where
  LoadType : Type
  idToFilepath : (id : String) -> String
  loadFilepath : (x : Var) -> (filepath : String) -> ST c r [x ::: LoadType]

  load : (x : Var) -> (id : String) -> ST c r [x ::: LoadType]
  load {c} {r} x id = loadFilepath x (idToFilepath {c} {r} id)

Если я удалю {c} {r} из определения load и вызову idToFilepath, этоне проверяет тип, выдавая следующее сообщение: 

Can't find implementation for Loader c r

В противном случае файл A проверяет тип.Это странно, но я видел, что передача косвенных значений в явном виде иногда может помочь.

Проблема в попытке реализации этого интерфейса в файле B .Несмотря на то, что определение интерфейса Loader в файле A проверяет типы, как только в файле B предпринимается попытка минимальной реализации, оно не проверяет типы.Вот код для справки: 

interface Draw (m : Type -> Type) where 
  -- ...

Draw m => Loader m Texture where
  LoadType {m} = ?check

Выдает следующее странное сообщение об ошибке: 

When checking left hand side of Resources.Main.m, Texture implementation of Resources.Loader, method load:
c is not an implicit argument of Resources.Main.m, Texture implementation of Resources.Loader, method load

Что не имеет смысла, учитывая, что файл A проверен и не провереносновной код был введен в B .

...