Подтвердить что ты не робот

Есть ли способ получить ошибку времени компиляции, если нет соответствующего экземпляра семейства закрытых типов?

У меня есть замкнутое семейство типов, которое не имеет особого случая:

{-# LANGUAGE TypeFamilies #-}

type family Foo a where
    Foo Bool = Int
    Foo Int = Bool

Есть ли способ заставить средство проверки типов отклонить следующую программу:

data T a = MkT deriving Show

x :: T (Foo String)
x = MkT

из-за того, что не существует типа Foo String?

Ответ 1

Начиная с GHC 8.0.1, можно написать:

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, UndecidableInstances #-}

import GHC.TypeLits

type family Foo a where
    Foo Bool = Int
    Foo Int  = Bool
    Foo a    = TypeError (Text "Invalid Foo " :<>: ShowType a)

data T a = MkT deriving Show

x :: T (Foo String)
x = MkT

Модуль может быть загружен, но вы не можете использовать x:

*Main> :r
[1 of 1] Compiling Main             ( te.hs, interpreted )
Ok, modules loaded: Main.
*Main> x

<interactive>:18:1: error:
    • Invalid Foo [Char]
    • When checking the inferred type
        it :: T (TypeError ...)

Если вы добавите без подписи типа

y = id x

GHC (i), пока они жалуются во время проверки типа:

te.hs:15:1: error:
    • Invalid Foo [Char]
    • When checking the inferred type
        y :: T (TypeError ...)

Однако, если вы дадите y тип: y :: T (Foo String); то GHC также примет это.

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