{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Data.Ten.Entails
( Entails(..), Dict1(..), (:!:)
, withEntailment, byEntailment
) where
import Data.Kind (Constraint)
import Data.Proxy (Proxy(..))
import Data.Type.Equality ((:~:)(..))
import Type.Reflection (TypeRep)
data Dict1 (c :: k -> Constraint) a = c a => Dict1
class Entails k c where
entailment :: k a -> Dict1 c a
instance (forall a. c a) => Entails TypeRep c where entailment :: TypeRep a -> Dict1 c a
entailment TypeRep a
_ = Dict1 c a
forall k (c :: k -> Constraint) (a :: k). c a => Dict1 c a
Dict1
instance (forall a. c a) => Entails Proxy c where entailment :: Proxy a -> Dict1 c a
entailment Proxy a
_ = Dict1 c a
forall k (c :: k -> Constraint) (a :: k). c a => Dict1 c a
Dict1
instance c a => Entails ((:~:) a) c where entailment :: (a :~: a) -> Dict1 c a
entailment a :~: a
Refl = Dict1 c a
forall k (c :: k -> Constraint) (a :: k). c a => Dict1 c a
Dict1
instance Entails (Dict1 c) c where entailment :: Dict1 c a -> Dict1 c a
entailment = Dict1 c a -> Dict1 c a
forall a. a -> a
id
class c (d a) => (c :!: d) a
instance c (d a) => (c :!: d) a
withEntailment :: forall c k a r. Entails k c => k a -> (c a => r) -> r
withEntailment :: k a -> (c a => r) -> r
withEntailment k a
k c a => r
r = case k a -> Dict1 c a
forall k (k :: k -> *) (c :: k -> Constraint) (a :: k).
Entails k c =>
k a -> Dict1 c a
entailment @_ @c k a
k of Dict1 c a
Dict1 -> r
c a => r
r
byEntailment :: forall c k a r. Entails k c => (c a => r) -> k a -> r
byEntailment :: (c a => r) -> k a -> r
byEntailment c a => r
r k a
k = k a -> (c a => r) -> r
forall k (c :: k -> Constraint) (k :: k -> *) (a :: k) r.
Entails k c =>
k a -> (c a => r) -> r
withEntailment @c k a
k c a => r
r