Ограничение на метод зависит от экземпляров в области?

Question

Рассмотрим этот код:

{-# language FlexibleInstances, UndecidableInstances #-}

module Y where

class C m where

    x :: m

instance {-# overlappable #-} Monoid m => C m where

    x = mempty

instance C Int where

    x = 53

Какого типа x?

λ :type x
x :: C m => m

Пока - все хорошо. Теперь удалите экземпляр Int. Какой тип x?

λ :type x
x :: Monoid m => m

Сюрприз!

Почему это происходит?

Answer 1

Это поведение объясняется в следующем сообщении в блоге:

• Синонимы непрозрачных ограничений

Вкратце: GHC достаточно умен, чтобы понять, чтоу вас есть только один экземпляр класса типов C и вы решили, что это единственный возможный экземпляр, поэтому каждый раз, когда он видит ограничение C m, он заменяет его на Monoid m, поскольку они эквивалентны.

NB Как далее объясняет @chi в комментарии:

Когда GHC находит ограничение C t, оно пытается его решить. Если if находит совпадение instance (...) => C t where ..., ограничение заменяется контекстом (...). Это повторяется в максимально возможной степени. Окончательное ограничение появляется в типе (или вызывает «неразрешенную» ошибку типа). Этот процесс оправдан, поскольку может быть только один совпадающий экземпляр. Перекрывающиеся экземпляры изменяют это и предотвращают это сокращение контекста, когда несколько экземпляров (в области действия!) Приблизительно совпадают. Это хрупкое расширение, которое следует использовать с осторожностью.