-- Copyright 2021 Google LLC
--
-- Licensed under the Apache License, Version 2.0 (the "License");
-- you may not use this file except in compliance with the License.
-- You may obtain a copy of the License at
--
--      http://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS,
-- WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
-- See the License for the specific language governing permissions and
-- limitations under the License.

{-# 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 #-}

-- | A typeclass of GADT-like types whose existence implies an instance.

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)

-- We could just use Dict from "constraints", but it'd be a dependency that we
-- don't really need to have.

-- | A dictionary for the given arity-1 constraint constructor ("a class").
data Dict1 (c :: k -> Constraint) a = c a => Dict1

-- | A typeclass of GADT-like types whose existence implies an instance.
--
-- For a trivial example, the existence of @Int :~: b@ implies @Show b@, since
-- we can discover that @b@ is @Int@ and use the @Show Int@ instance.
class Entails k c where
  entailment :: k a -> Dict1 c a

-- | Non-GADTy types don't entail anything except parametric instances.
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

-- | Equality to a particular type entails any instance that type has.
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

-- | 'Dict1's entail their own type parameter.
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

-- | A utility "typeclass newtype" that's convenient with 'Entails'.
--
-- If you want to use 'entailment' to get an instance of the form @c (d a)@,
-- use @entailment \@(c :!: d)@.  Really I wanted to use the name (@:.:@), but
-- it's taken, so I just replaced the period with something else that involves
-- a dot near the typographic base line.
class c (d a) => (c :!: d) a
instance c (d a) => (c :!: d) a

-- | Bring an instance into scope using an 'Entails' instance.
--
-- @
--     (\ (k :: Int :~: b) (x :: b) -> withEntailment @Show k (show x)) Refl 2
-- @
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

-- | @flip 'withEntailment'@.
--
-- This is useful for "consuming" an index off the front of a function type and
-- turning it into an instance, e.g. in the context of an
-- 'Data.Ten.Functor.WithIndex.imap10' call.
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