little exercise in constrained existential types

constraint_existentials.hs

data E (c :: k -> Constraint) (f :: k -> Type) = forall a . c a => E { unE :: f a }

runE :: forall b c f . (forall a . c a => f a -> b) -> E c f -> b
runE g (E a) = g a

-- this says that when I have a value of type 'E c f' where 'c' is a type-level function from kinds to constraints
-- and 'f' is a data type with one kind parameter, then I can apply any function
-- 
-- @
-- g :: forall a . c a => f a -> b
-- @
-- 
-- on that value.
-- the type 'a' is not statically known and can be anything that fulfills the constraint

newtype UnknownDeviceTensor device = UnknownDeviceTensor { unWrap :: Tensor device 'D.Float '[] } 

test :: E KnownDevice UnknownDeviceTensor -> D.Device
test = runE (device . unWrap)

-- of course, in the example 'test' I’m cheating a bit.
-- Because, in order to get a value of E KnownDevice UnknownDeviceTensor, I need to know the device:
mkE :: E KnownDevice UnknownDeviceTensor
mkE = E (UnknownDeviceTensor (ones @'[] @'D.Float @'( 'D.CPU, 0)))