Как извлечь информацию о типе из Proxy в семействе типов для GADT? - PullRequest
Новая
       42

Как извлечь информацию о типе из Proxy в семействе типов для GADT?

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

У меня есть следующий фрагмент: 

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}

import Data.Proxy

data Foo where
  FooInt :: Foo
  FooProxy :: IsEnum e ~ True => Proxy e -> Foo

type family IsEnum e :: Bool

type family FromFoo (foo :: Foo) where
  FromFoo FooInt = Int
  FromFoo (FooProxy ('Proxy :: Proxy e)) = e

Общая идея заключается в том, что я пытаюсь использовать Foo в качестве вида данных, где я могу сделать 

type MyFoo1 = FooInt :: Foo
type instance IsEnum Bool = True
type MyFoo2 = FooProxy ('Proxy :: Proxy Bool) :: Foo

иубедитесь, что прокси-тип, передаваемый в FooProxy, является частью семейства IsEnum (я не могу просто сделать FooProxy :: Enum e => Proxy e -> Foo, потому что в настоящее время поддерживаются только ограничения равенства ).

Но когда я пытаюсь скомпилировать это, я получаю сообщение об ошибке: 

<interactive>:30:12: error:
    • Couldn't match expected kind ‘'True’ with actual kind ‘IsEnum e’
    • In the first argument of ‘FromFoo’, namely
        ‘(FooProxy ( 'Proxy :: Proxy e))’
      In the type family declaration for ‘FromFoo’

Проблема заключается в том, что я хочу преобразовать тип Foo в конкретный тип в FromFoo, я хочу FooProxy для оценки по типу прокси.Поэтому я пытаюсь сопоставить шаблон с Proxy, чтобы вернуть прокси-тип e, но затем, похоже, снова проверяется ограничение IsEnum e ~ True.Я бы подумал, что ограничение будет проверяться только при создании FooProxy значения, но, похоже, проверяется снова, когда сопоставление с шаблоном .

...