Когда GHC может определить переменные ограничения?

Question

Я получаю ошибки вывода типа, потому что GHC не выведет переменную ограничения. Это выглядит выводимым за счет объединения первого порядка. В ходе дальнейшего исследования я обнаружил, что вставка привязок позволяет изменить поведение вывода типов. Я хотел бы знать, что делает GHC.

Код здесь демонстрирует проблему. Новый тип ConstrainedF c обозначает полиморфную функцию, параметр типа которой ограничен c, Насколько я могу судить, GHC не будет делать вывод c на основе значений, данных для ConstrainedF,

{-# LANGUAGE RankNTypes, ScopedTypeVariables, ConstraintKinds, MonoLocalBinds #-}

import Data.Monoid
import GHC.Prim(Constraint)

newtype ConstrainedF c =
  ConstrainedF { runConstrainedF :: forall a. c a => [a] -> a}

applyConstrainedF :: forall c a. c a => ConstrainedF c -> [a] -> a
applyConstrainedF f xs = runConstrainedF f xs

-- GHC cannot infer the type parameter of ConstrainedF
foo :: [Int]
foo = applyConstrainedF (ConstrainedF mconcat) [[1], [2]]
--foo = applyConstrainedF (ConstrainedF mconcat :: ConstrainedF Monoid) [[1], [2]]

Должно быть возможно вывести типы в приложении ConstrainedF mconcat:

1. ConstrainedF имеет тип forall c. (forall a. c a => [a] -> a) -> ConstrainedF c,
2. mconcat имеет тип forall b. Monoid b => [b] -> b,
3. forall b. Monoid b => [b] -> b объединяется с forall a. c a => [a] -> a по заданию a := b а также c := Monoid,

Однако GHC жалуется:

Could not deduce (Monoid a) arising from a use of `mconcat'
from the context (c0 a).

Каким правилам я должен следовать в отношении переменных ограничений, чтобы GHC мог выводить типы?

---

Типичным решением для ошибок неоднозначного типа является добавление значений прокси для ограничения неоднозначного типа. Это было привередливо, когда я попробовал это. Если я просто добавлю дополнительный параметр, чтобы ограничить тип c, оно работает:

data Cst1 (c :: * -> Constraint) = Cst1

monoid :: Cst1 Monoid
monoid = Cst1

applyConstrainedF :: forall c a. c a => ConstrainedF c -> Cst1 c -> [a] -> a
applyConstrainedF f _ xs = runConstrainedF f xs

foo :: [Int]
foo = applyConstrainedF (ConstrainedF mconcat) monoid [[1], [2]]

Но введение привязки пусть в foo путает вывод типа, и он больше не может объединять c с Monoid,

foo_doesn't_work :: [Int]
foo_doesn't_work = let cf = ConstrainedF mconcat
                   in applyConstrainedF cf monoid [[1], [2]]

Поскольку вывод типа дает правильный ответ в одной из этих двух функций, это говорит мне о том, что GHC будет унифицировать переменные ограничения в некоторых ситуациях, но не в других. Я не понимаю, что происходит.

Answer 1

Проблема здесь в подтипах. В вашем примере c может быть (Monoid b, Eq b),

Кроме того, вы можете использовать Data.Typeable осмотреть что c был создан с.

Или, что если бы вы попросили "объединить" (c, d) (пара ограничений) с Monoid?

---

Ответ на вторую часть вашего вопроса - вы догадались! - позвольте обобщение.

Я знаю, что вы догадались, так как вы добавили MonoLocalBinds Прагма. Тем не менее, он не делает то, что вы ожидаете здесь. Видите ли, он только останавливает обобщение истинно локальных привязок, которые зависят от параметров функции или других локальных привязок.

Например, это работает:

foo_does_work :: () -> [Int]
foo_does_work x =
  let cf = const (ConstrainedF mconcat) x
  in applyConstrainedF cf monoid [[1], [2]]

Подробности см. В разделе Обобщение: на какие привязки влияют?