Skip to content

Floating 'forall x. Dict (cls x)' inwards 'Dict (forall x. cls x)'

This is more of an inquiry than an issue,

  1. Is it sound to float the quantifier in forall x. Dict (cls x) into the dict: Dict (forall x. cls x)
  2. If sound, is it possible to implement this float function in GHC?
  3. 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
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information