Как я могу дать подсистеме логического вывода некоторые подсказки?

Question

В (очень) современных GHC я могу написать это:

{-# LANGUAGE TypeFamilies #-}

-- consider this part "library" code, changeable at will
data Container a = Container
data Element
class Foo a where foo :: a -> Int
instance Element ~ a => Foo (Container a) where foo _ = 0

-- consider this part "client" code; bonus points if it can remain exactly as is
main = print (foo Container)

Существенные моменты:

1. Код клиента не требует никаких дополнительных подписей типа.
2. Container, то есть полиморфное значение (типа Container a), было правильно мономорфно в Container Element.
3. В клиентском коде не требовались оболочки нового типа.
4. Вероятно, невозможно объявить другой экземпляр Foo, конструктор внешнего типа которого равен Container.Это , а не свойство, которое я хочу сохранить в следующем обсуждении.

Можно ли сделать это более обратно совместимым способом?Моя первая попытка выглядела так:

{-# LANGUAGE FlexibleInstances #-}

data Container a = Container
data Element
class Foo a where foo :: a -> Int
instance Foo (Container Element) where foo _ = 0

main = print (foo Container)

..., которая выдает ошибку:

test.hs:8:15:
    No instance for (Foo (Container a0))
      arising from a use of `foo'
    Possible fix: add an instance declaration for (Foo (Container a0))
    In the first argument of `print', namely `(foo Container)'
    In the expression: print (foo Container)
    In an equation for `main': main = print (foo Container)

Я понял, что эта ошибка, вероятно, возникает, потому что экземпляр не использует переменную типав качестве аргумента Container, поэтому я также попытался:

{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, UndecidableInstances #-}

data Container a = Container
data Element
class Foo a where foo :: a -> Int
instance Convertible a Element => Foo (Container a) where foo _ = 0
class Convertible a b where
    -- convert is not necessary in this tiny example, but it would
    -- be necessary in my not-so-tiny use case
    convert :: Container a -> Container b
instance Convertible a a where
    convert = id

main = print (foo Container)

Но это только подталкивает проблему к классу типа Convertible:

test.hs:14:19:
    No instance for (Convertible a0 Element)
      arising from a use of `foo'
    Possible fix:
      add an instance declaration for (Convertible a0 Element)
    In the first argument of `print', namely `(foo Container)'
    In the expression: print (foo Container)
    In an equation for `main': main = print (foo Container)

Похожая ошибка возникает изнаписание экземпляра для Convertible Element Element вместо Convertible a a.Моя последняя попытка заключалась в том, чтобы специализироваться еще дальше:

data Container a = Container
data Element
class Foo a where foo :: a -> Int
instance IsElement a => Foo (Container a) where foo _ = 0
class IsElement a where
    convert :: a -> Element
instance IsElement Element where
    convert = id

main = print (foo Container)

..., который имеет заметное преимущество в виде H98, но заметный недостаток по-прежнему не совсем работает:

test.hs:10:19:
    Ambiguous type variable `a0' in the constraint:
      (IsElement a0) arising from a use of `foo'
    Probable fix: add a type signature that fixes these type variable(s)
    In the first argument of `print', namely `(foo Container)'
    In the expression: print (foo Container)
    In an equation for `main': main = print (foo Container)

Итак, вопрос в следующем: есть ли подобная реализация, которая достигает свойств 1, 2 и 3, описанных выше, но не требует оператора равенства типов?

edit Я думал, что ранг-2 типа могут помочь:

{-# LANGUAGE FlexibleInstances, RankNTypes #-}

data Container a = Container
data Element
class Foo a where foo :: a -> Int
instance Foo (forall a. Container a) where foo _ = 0

main = print (foo Container)

... но, увы, по-прежнему нет кости:

test.hs:6:14:
    Illegal polymorphic or qualified type: forall a. Container a
    In the instance declaration for `Foo (forall a. Container a)'

Answer 1

Я не понимаю, что вы пытаетесь сделать здесь.В частности, почему вас волнует, что Container является полиморфным, когда вы хотите, чтобы клиент работал только с Container Element?

Тем не менее, как насчет использования другого типа для класса типов?

data Container a = Container
data Element

class Foo a where foo :: a x -> Int

instance Foo Container where foo _ = 0

Теперь действительно не имеет значения, для какого типа создан экземпляр Container.

Если это не сработает, я подозреваю, что ответ «нет, вы не можете делать именно то, что хотите."Хотя вы можете экспортировать container = Container :: Container Element и использовать клиентский код вместо Container.

Edit: с учетом полного контекста и невозможности использования типов ранга 2, я вполне уверен, чтоне является решением с учетом проблемных ограничений.Лучший способ обойти это - создать новую функцию xcast :: XConfig a -> XConfig Layout.Это позволит вам написать instance Binding (XConfig a -> Foo).