uninstantiable family for safe polykinded universally quantified constraints?

Forall.hs

{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds, Rank2Types,
  ScopedTypeVariables #-}

{-# LANGUAGE FlexibleInstances, UndecidableInstances, MultiParamTypeClasses
  #-} -- only for examples

module Proposed.Data.Constraint.Forall
  (module Data.Constraint,
   Forall, Bottom, inst) where

import Unsafe.Coerce (unsafeCoerce)

import Data.Constraint (Dict(..), Constraint)


-- | Seriously, do not instantiate this type family; it is a source of
-- polykinded skolem variables, and soundness is compromised if it is
-- instantiated.
type family DO_NOT_INSTANTIATE (x :: k -> Constraint) :: k

-- safe to export, since
--
-- 1) it can't be used to instantiate the family
-- 2) it can't be used to decompose the skolems (family not injective)
--
-- ... right?
type Bottom x = DO_NOT_INSTANTIATE x



-- safe because @Bottom p@ is irreducible and not a value (ie not a type
-- constructor); ie it's a skolem type term. Thus @Forall p@ is satisfied iff
-- @p@ is parametric wrt its next parameter.
--
-- Only nestings of @Forall@ could possibly result in the unsound reuse of the
-- same skolem type term for distinct quantified variables, but that nesting is
-- prevented by making @p@ a parameter to @Bottom@ -- explained below.
inst :: forall p t. Forall p => Dict (p t)
inst = unsafeCoerce (Dict :: Dict (p (Bottom p)))



-- WWe include the constraint itself in the skolem variable's syntactic
-- representation. This makes all skolem variables in scope distinct when
-- @Forall@s are nested. Such nesting is required in order for the use of
-- @unsafeCoerce@ in @inst@ to be unsound. But the construction of such
-- nestings requires intermediate class definitions (like @Forall2@ below) in
-- order to thread through the environment of other quantified
-- variables. Because those threading classes now end up as part of each skolem
-- type's syntactic representation, each variable in the environment is
-- syntactically distinct, and so soundness is maintained.
type Forall (p :: k -> Constraint) = p (Bottom p)




data Proxy (t :: k) = Proxy
class C (t :: k) where
  method :: Proxy t -> String

instance C (t :: *) where
  method _ = "*"

instance Functor t => C (t :: * -> *) where
  method _ = "functor"

test_good = case inst :: Dict (C Int) of Dict -> method (Proxy :: Proxy Int)

-- ill-typed
-- test_bad = case inst :: Dict (C []) of Dict -> method (Proxy :: Proxy [])





class EQ (a :: *) (b :: *) where cast :: a -> b
instance EQ a a where cast = id



class    Forall (c a) => Forall2 c a
instance Forall (c a) => Forall2 c a

-- ill-typed with this implementation; would be well-typed if @Bottom@ took no
-- argument
--
--test_evil :: Int
--test_evil = case inst :: Dict (Forall2 EQ Char) of
--  Dict -> case inst :: Dict (EQ Char Int) of
--    Dict -> cast 'c'
--
--    No instance for (EQ
--                        (DO_NOT_INSTANTIATE (Forall2 EQ))
--                        (DO_NOT_INSTANTIATE
--                           (EQ (DO_NOT_INSTANTIATE (Forall2 EQ)))))

ForallN.hs

-- this files supplants these definitions from the constraints package:
--
-- type ForallF (p :: * -> Constraint) (f :: * -> *) = (p (f A), p (f B))
-- type ForallT (p :: * -> Constraint) (t :: (* -> *) -> * -> *) = (p (t F A), p (t M B))
--
-- as well as instF and instT

-- an auxiliary for ForallF
class    p (f a) => CompositionInOne p f a
instance p (f a) => CompositionInOne p f a

type ForallF p f = Forall (CompositionInOne p f)

instF :: forall p f a. ForallF p f => Dict (p (f a))
instF = case inst :: Dict (CompositionInOne p f a) of
          Dict -> Dict



test_monoid :: forall f a. ForallF Monoid f => Dict (Monoid (f a))
test_monoid = instF



-- using nesting for two quantifiers
class    Forall (p a) => Forall_Once_Nested p a
instance Forall (p a) => Forall_Once_Nested p a

type Forall2 p = Forall (Forall_Once_Nested p)

inst2 :: forall p a b. Forall2 p => Dict (p a b)
inst2 = case inst :: Dict (Forall_Once_Nested p a) of
          Dict -> case inst :: Dict (p a b) of
            Dict -> Dict


-- an auxiliary for ForallT
class    p (t a b) => CompositionInTwo p t a b
instance p (t a b) => CompositionInTwo p t a b

type ForallT p t = Forall2 (CompositionInTwo p t)

instT :: forall p t a b. ForallT p t => Dict (p (t a b))
instT = case inst2 :: Dict (CompositionInTwo p t a b) of
          Dict -> Dict