Forgetting the types on a mapped HList

Example.hs

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Example where

import Data.Kind
import Data.Coerce

data HList (l :: [Type]) where
    HNil  :: HList '[]
    HCons :: e -> HList l -> HList (e ': l)

type family Map (f :: k1 -> k2) (xs :: [k1]) :: [k2] where
   Map f '[]       = '[]
   Map f (x ': xs) = f x ': Map f xs

newtype TypedWrapper ty = TypedWrapper Int
data Example (ts :: [Type]) = Example { typedWrappers :: HList (Map TypedWrapper ts) }

-- Typeclass approach

class HCoerceOut1 (l :: [Type]) (o :: Type) where
    hCoerceOut1 :: HList l -> [o]

instance HCoerceOut1 '[] o where
    hCoerceOut1 HNil = []

instance (HCoerceOut1 l o, Coercible e o) => HCoerceOut1 (e ': l) o where
    hCoerceOut1 (HCons e l) = coerce e : hCoerceOut1 l

toUntyped1 :: Example ts -> [Int]
toUntyped1 (Example wrapped) = hCoerceOut1 wrapped

{-
Example.hs:40:32: error:
    • No instance for (HCoerceOut1 (Map TypedWrapper ts) Int)
        arising from a use of ‘hCoerceOut1’
    • In the expression: hCoerceOut1 wrapped
      In an equation for ‘toUntyped1’:
          toUntyped1 (Example wrapped) = hCoerceOut1 wrapped
   |
40 | toUntyped1 (Example wrapped) = hCoerceOut1 wrapped
   |                               ^^^^^^^^^^^^^^^^^^
-}

-- 'All' approach

type family All (c :: Type -> Constraint) (ts :: [Type]) :: Constraint where
    All c '[] = ()
    All c (t ': ts) = (c t, All c ts)

hCoerceOut2 :: forall (ts :: [Type]) o . All (Coercible o) ts => HList ts -> [o]
hCoerceOut2 HNil = []
hCoerceOut2 (HCons e es) = coerce e : hCoerceOut2 es

toUntyped2 :: Example ts -> [Int]
toUntyped2 (Example wrapped) = hCoerceOut2 wrapped

{-
Example.hs:53:32: error:
    • Could not deduce: All (Coercible Int) (Map TypedWrapper ts)
        arising from a use of ‘hCoerceOut2’
    • In the expression: hCoerceOut2 wrapped
      In an equation for ‘toUntyped2’:
          toUntyped2 (Example wrapped) = hCoerceOut2 wrapped
    • Relevant bindings include
        wrapped :: HList (Map TypedWrapper ts)
          (bound at ledger/Ledger/Typed/Example.hs:53:21)
        toUntyped2 :: Example ts -> [Int]
          (bound at ledger/Ledger/Typed/Example.hs:53:1)
   |
53 | toUntyped2 (Example wrapped) = hCoerceOut2 wrapped
   |                                ^^^^^^^^^^^^^^^^^^^
-}