Неоднозначный тип с использованием явных квантификаторов

Использование ScopedTypeVariables здесь не помогает, потому что p, которое вы используете, в любом случае, похоже, не входит в область действия. Сравните следующие определения:

changeBase (ZqBasic x) = fromIntegral (value (undefined::foobar))

Это дает ту же ошибку, потому что также создает переменную нового типа.

changeBase (ZqBasic x) = fromIntegral (value (5::p))

Однако это дает другую ошибку. Соответствующие биты:

Could not deduce (Num p1) arising from the literal `5'
        (snip)
    or from (Zq q (ZqBasic q a), Zq p b)
      bound by the type signature for
                 changeBase :: (Zq q (ZqBasic q a), Zq p b) => ZqBasic q a -> b

Это показывает, что p создается как переменная нового типа. Я предполагаю, что forall в сигнатуре типа не включает в область действия (в фактических объявлениях) переменные типа, которые не являются параметрами типа класса. Однако он действительно делает переменную областью действия для объявления по умолчанию.

Во всяком случае, это ни здесь, ни там.

Достаточно легко обойти большинство проблем, связанных с необходимостью доступа к переменным типа, — просто создайте несколько вспомогательных функций, которые ничего не делают, но позволяют вам соответствующим образом манипулировать типами. Например, бессмысленная функция, подобная этой, будет притворяться, что вызывает в воображении терм с фантомным типом:

zq :: (Zq q a) => a -> q
zq _ = undefined

По сути, это просто дает вам прямой доступ на уровне терминов к функциональной зависимости, поскольку fundep делает q однозначным для любого конкретного a. Вы не можете получить фактическое значение, конечно, но это не главное. Если вас беспокоит undefined, используйте вместо этого [] :: [q] для аналогичного эффекта и используйте head или что-то еще, только когда вам нужно.

Теперь вы можете немного изменить ситуацию, используя предложение where или что-то еще, чтобы принудительно вывести правильные типы:

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase (ZqBasic x) = b
    where b = fromIntegral (value (zq b))

Здесь происходит то, что b — это действительно то, что нам нужно, но нам нужно value, чтобы увидеть тип p, который определяется типом b, поэтому, назначив временное имя результату, мы можем использовать его для получения типа, который мы нужно.

Во многих случаях вы также можете сделать это без дополнительного определения, но с классами типов вам нужно избегать специального полиморфизма и гарантировать, что он не позволяет «рекурсии» включать другие экземпляры.

В связи с этим функция стандартной библиотеки asTypeOf предназначена именно для такого типа возни с типами.

Вызов value (undefined::p) преобразует p в некоторый тип a0. Из типа value единственное, что мы можем понять, это то, что a0 является целочисленным типом.

Это значение передается в fromIntegral, который преобразует a0 в b. Из типа fromIntegral единственное, что мы можем понять, это то, что a0 является целочисленным типом.

Ничто не определяет тип a0, поэтому для разрешения неоднозначности необходима аннотация типа в выражении value (undefined::p). Глядя на ваши сигнатуры типов, похоже, что value должен иметь возможность генерировать правильный тип возвращаемого значения без каких-либо дополнительных преобразований. Можете ли вы просто удалить вызов fromIntegral?

Изменить

Вам необходимо включить расширение ScopedTypeVariables. Без ScopedTypeVariables переменная типа не может упоминаться более чем в одной сигнатуре типа. В этом случае имя переменной p не ссылается на одну и ту же переменную в сигнатуре типа функции и в ее теле.

У меня работает следующий код:

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase = zqBasicChangeBase

zqBasicChangeBase :: forall p b q a.
  (IntegralAsType q, IntegralAsType p, Integral a, Zq p b) => ZqBasic q a -> b
zqBasicChangeBase (ZqBasic x) = fromIntegral (value (undefined :: p) :: Integer)

Два (по существу эквивалентных?) подхода, которые работают:

1: Использование К.А. Подход Макканна:

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase (ZqBasic x) = b
    where b = fromIntegral ((value (zq b))*(fromIntegral (value (zq q)))) -- note that 'q' IS in scope

2: Вместо подписи a->b я изменил подпись changeBase на b->a Затем работает следующее:

instance (IntegralAsType q, Integral a) => Zq q (ZqBasic q a) where
  changeBase x = fromIntegral ((value (zq x))*(fromIntegral (value (zq q)))) -- note that 'q' IS in scope

Цель всегда состояла в том, чтобы иметь доступ к параметрам типа как для аргумента, так и для типа возвращаемого значения, и оба этих подхода позволяют мне это сделать.

Кроме того, ответ на мой вопрос о разнице между конструктором «zqBasic» и «changeBase», как указал C.A.McAnn, заключается в том, что «p» не помещается в область видимости в объявлениях, даже с явным forall. Если кто-нибудь может объяснить, почему это так, буду признателен.