Как использовать UndecidableInstances локально?

Question

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

instance Foo x (C x y) => Bar (C x y) where

    ...

и его изменение сделало бы API значительно уродливее. Я никогда не получаю Foo из Bar, поэтому нет никакого способа сделать цикл.

С другой стороны, включение UndecidableInstances позволяет легко игнорировать глупые ошибки. Например, я мог написать по ошибке что-то вроде:

instance Foo x (C x z) => Bar (C x y) where

    ...

, где z никогда не появляется с правой стороны.

Вопрос: Можно ли использовать UndecidableInstances локально в модуле, т. Е. Явно отмечать места, где отменены обычные правила завершения?

Конечно, это не поможет с прекращением, но примет решение использовать это расширение более информированно.

Вопрос 2: Есть ли что-то более слабое, чем UndecidableInstances, которое все еще не гарантировало бы завершение, но запретило бы некоторые более пограничные случаи, такие как второй фрагмент кода?

Answer 1

До сих пор языковые прагмы были для каждого модуля, поэтому ответ на первый вопрос - нет.Что касается второго вопроса, я не совсем уверен, но я не знаю другого расширения, кроме UndecidableInstances, которое бы разрешало экземпляр.

Однако UndecidableInstances не так уж и плох, он просто позволяет средству проверки типапопытаться разрешить случаи, когда он не может доказать прекращение.Тем не менее, контекстный стек предотвращает его зацикливание.