добавление сигнатуры выводимого типа ghci приводит к ошибке - PullRequest
Новая
       11

добавление сигнатуры выводимого типа ghci приводит к ошибке

9 голосов
/ 16 декабря 2011

Редактировать: Вот действительно простой пример. Мотивация для этого примера ниже.

Это компилируется: 

{-# LANGUAGE TypeFamilies #-}

type family F a b

f :: a -> F a b
f = undefined

f' [a] = f a

И GHCI сообщает, что: 

*Main> :t f'
f' :: [a] -> F a b

Но если мы добавим сигнатуру этого типа в файл выше, он пожалуется: 

*Main> :r
[1 of 1] Compiling Main             ( test.hs, interpreted )

test.hs:9:14:
    Couldn't match type `F a b0' with `F a b'
    NB: `F' is a type function, and may not be injective
    In the return type of a call of `f'
    In the expression: f a
    In an equation for `f'': f' [a] = f a
Failed, modules loaded: none.

Что дает?

Мотивация:

Увидев этот вопрос , я подумал, что стану умным Алеком и напишу небольшое решение для шутки. План атаки состоит в том, чтобы начать с чисел уровня типа (как обычно), затем написать небольшую функцию уровня типа Args n a c, которая возвращает тип функции, который принимает n копий a и дает c. Тогда мы можем написать небольшой класс типов для различных n и быть в пути. Вот что я хочу написать: 

{-# LANGUAGE TypeFamilies #-}

data Z = Z
data S a = S a

type family Args n a c
type instance Args Z a c = c
type instance Args (S n) a c = a -> Args n a c

class OnAll n where
    onAll :: n -> (b -> a) -> Args n a c -> Args n b c

instance OnAll Z where
    onAll Z f c = c

instance OnAll n => OnAll (S n) where
    onAll (S n) f g b = onAll n f (g (f b))

Я был удивлен, обнаружив, что это не проверка типа!

1 Ответ

9 голосов
/ 16 декабря 2011

Это ошибка GHC, о чем свидетельствует следующий, еще более упрощенный пример: 

type family F a

f :: b -> F a
f = undefined

f' :: b -> F a
f' a = f a

Я предлагаю сообщить об этом в штаб-квартиру GHC.

...