Странное сообщение об ошибке GHC, "Мой мозг только что взорвался"?

Question

Когда я пытаюсь сопоставить шаблон GADT в proc синтаксис (с Netwire и Vinyl):

sceneRoot = proc inputs -> do
            let (Identity camera :& Identity children) = inputs 
            returnA -< (<*>) (map (rGet draw) children) . pure

Я получаю (довольно странную) ошибку компилятора из ghc-7.6.3

  Мой мозг только что взорвался
    Я не могу обработать привязки к шаблону для конструкторов GADT или экзистенциальных данных.
    Вместо этого используйте case-выражение или do-notation, чтобы распаковать конструктор.
    В шаблоне: Идентификационная камера:& Идентификационные данные ребенка

Я получаю похожую ошибку, когда я помещаю шаблон в proc (...) шаблон. Почему это? Это несостоятельно или просто не реализовано?

Answer 1

Рассмотрим ГАДТ

data S a where
  S :: Show a => S a

и выполнение кода

foo :: S a -> a -> String
foo s x = case s of
            S -> show x

В реализации Haskell на основе словаря можно ожидать, что значение s несет словарь класса, и что case извлекает show функция из указанного словаря, так что show x может быть выполнено.

Если мы выполним

foo undefined (\x::Int -> 4::Int)

мы получаем исключение. В оперативном плане это ожидается, потому что мы не можем получить доступ к словарю. Больше в общем, case (undefined :: T) of K -> ... будет выдавать ошибку, потому что это вызывает оценку undefined (при условии, что T это не newtype).

Теперь рассмотрим код (давайте представим, что он компилируется)

bar :: S a -> a -> String
bar s x = let S = s in show x

и исполнение

bar undefined (\x::Int -> 4::Int)

Что это должно сделать? Можно утверждать, что он должен генерировать то же исключение, что и с foo, Если бы это было так, ссылочная прозрачность означала бы, что

let S = undefined :: S (Int->Int) in show (\x::Int -> 4::Int)

сбои также с тем же исключением. Это будет означать, что let оценивает undefined выражение, в отличие от, например,

let [] = undefined :: [Int] in 5

который оценивает 5,

Действительно, шаблоны в let ленивы: они не форсируют оценку выражения, в отличие от case, Вот почему, например,

let (x,y) = undefined :: (Int,Char) in 5

успешно оценивает 5,

Можно хотеть сделать let S = e in e' оценивать e если show нужен в e', но это кажется довольно странным. Также при оценке let S = e1 ; S = e2 in show ... было бы неясно, стоит ли оценивать e1, e2, или оба.

GHC на данный момент решает запретить все эти случаи с помощью простого правила: никаких ленивых шаблонов при устранении GADT.