How do I extract type information from Proxy in a type family for a GADT?

Question

I have the following snippet:

{-# 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

The general idea is that I'm trying to use Foo as a data kind where I could do

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

and ensure that the proxied type being passed to FooProxy is a part of the IsEnum type family (I can't just do FooProxy :: Enum e => Proxy e -> Foo because only equality constraints are currently supported).

But when I try to compile this, I get the error:

<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’

The problem is when I want to convert from my Foo type to the concrete type in FromFoo, I want FooProxy to evaluate to the proxied type. So I'm trying to pattern match on Proxy to return the proxied type e, but then it seems to be checking the IsEnum e ~ True constraint again. I would think that the constraint would only be checked when creating a FooProxy value, but it seems to be checking again when pattern matching.