Floating 'forall x. Dict (cls x)' inwards 'Dict (forall x. cls x)'
This is more of an inquiry than an issue,
- Is it sound to float the quantifier in
forall x. Dict (cls x)
into the dict:Dict (forall x. cls x)
- If sound, is it possible to implement this
float
function in GHC? - If not possible, what modification to the surface language would allow it?
Here is an example program where we are able to define a Dict (cls a)
for any a
. Question 1. asks if float = unsafeCoerce
is correct:
{-# Language ConstraintKinds #-}
{-# Language GADTs #-}
{-# Language ImpredicativeTypes #-}
{-# Language InstanceSigs #-}
{-# Language StandaloneKindSignatures #-}
import Data.Kind
import Unsafe.Coerce
type Dict :: Constraint -> Type
data Dict cls where
Dict :: cls => Dict cls
type AlwaysList :: (Type -> Constraint) -> Constraint
class AlwaysList cls where
alwaysList :: Dict (cls [a])
instance AlwaysList Semigroup where
alwaysList :: Dict (Semigroup [a])
alwaysList = Dict
instance AlwaysList Monoid where
alwaysList :: Dict (Monoid [a])
alwaysList = Dict
-- float alwaysList :: AlwaysList cls => Dict (forall x. cls [x])
float :: (forall x. Dict (cls [x])) -> Dict (forall x. cls [x])
float = unsafeCoerce