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

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

{-# 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, но, похоже, оно проверяется снова при сопоставлении шаблона.