{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Datafix.Utils.Constraints
( Dict (..)
, (:-) (..)
, (\\)
, Forall
, inst
) where
import Data.Kind
import Unsafe.Coerce (unsafeCoerce)
data Dict :: Constraint -> Type where
Dict :: c => Dict c
newtype a :- b = Sub (a => Dict b)
infixl 1 \\
(\\) :: a => (b => r) -> (a :- b) -> r
r \\ Sub Dict = r
type family Skolem (p :: k -> Constraint) :: k
type family Forall (p :: k -> Constraint) :: Constraint
type instance Forall p = Forall_ p
class p (Skolem p) => Forall_ (p :: k -> Constraint)
instance p (Skolem p) => Forall_ (p :: k -> Constraint)
inst :: forall p a . Forall p :- p a
inst = unsafeCoerce (Sub Dict :: Forall p :- p (Skolem p))