GHC завис из-за UndecidableSuperClasses - ожидаемое поведение или ошибка? - PullRequest
0 голосов
/ 29 ноября 2018

Следующий фрагмент приводит к зависанию GHC (проверено с помощью 8.6.2 и 8.4.4) во время компиляции:

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}

import GHC.Exts (Constraint)

data T = T

type family F t (c :: * -> Constraint) :: Constraint
type instance F T c = c T

class F t C => C t where

t :: C T => t
t = undefined

Я думаю, что оно застревает, потому что для t GHC пытается найти C T, что приводит к F T C, который расширяется с помощью семейства типов F обратно до C T, что и требовалось (бесконечный цикл).

Я полагаю, что теоретически GHC мог бы сказать, что он достиг своегостремиться к C T от самого себя и что все, что зависит от него самого, может нормально работать рекурсивно, или я что-то неправильно понимаю?

Примечание: в реальном примере, где я наткнулся на это поведение, я смог достичь того, чегоЯ хотел, чтобы компилятор не зависал, заменив UndecidableSuperClasses на Data.Constraint.Dict.

1 Ответ

0 голосов
/ 29 ноября 2018

UndecidableSuperClasses делает не делает разрешение экземпляра ленивым.Компилятор по-прежнему будет расширять ограничения суперкласса, насколько это возможно.Я считаю, что поля в словарях экземпляров, которые указывают на словари суперкласса, строгие , и GHC фактически связывает их во время компиляции.Это отличается от UndecidableInstances, который позволяет ограничения экземпляров обрабатывать (немного) лениво.

deriving instance Show (f (Fix f)) => Show (Fix f)

будет работать просто отлично.При разрешении экземпляра, например, Show (Fix Maybe)), GHC увидит, что ему нужно Show (Maybe (Fix Maybe)).Затем он видит, что ему нужно Show (Fix Maybe) (что он в настоящее время разрешает), и принимает, что благодаря UndecidableInstances.

Все, что делает UndecidableSuperClases, отключает проверки, гарантирующие, что расширение не будет зацикливаться.Смотрите бит в начале выступления Эда Кметта , где он описывает процесс «достижения фиксированной точки».

Рассмотрим рабочий пример (извлечено из Data.Constraint.Forall):

type family Skolem (p :: k -> Constraint) :: k
class p (Skolem p) => Forall (p :: k -> Constraint)

GHC принимает это только с UndecidableSuperclasses.Зачем?Потому что он ничего не знает о том, что может означать это ограничение.Насколько он знает, это может быть случай, когда p (Skolem p) уменьшится до Forall p.И это действительно может произойти!

class Forall P => P x

-- This definition loops the type checker
foo :: P x => x
foo = undefined
...