-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- | General type utilities.
module Morley.Util.Type
  ( IsEq
  , type (==)
  , If
  , type (++)
  , IsElem
  , type (/)
  , type (//)
  , AssertTypesEqual
  , FailUnlessEqual
  , FailUnlessEqualElse
  , Guard
  , FailWhen
  , FailWhenElse
  , FailWhenElsePoly
  , FailUnless
  , FailUnlessElse
  , FailUnlessElsePoly
  , failUnlessEvi
  , failWhenEvi
  , AllUnique
  , RequireAllUnique
  , ReifyList (..)
  , PatternMatch
  , PatternMatchL
  , KnownList (..)
  , KList (..)
  , RSplit
  , rsplit
  , Some1 (..)
  , recordToSomeList

  , ConcatListOfTypesAssociativity
  , listOfTypesConcatAssociativityAxiom

  , MockableConstraint (..)

  , onFirst
  , knownListFromSingI
  ) where

import Data.Constraint (Dict(..), (:-)(..), (\\))
import Data.Eq.Singletons (DefaultEq)
import Data.Singletons (SingI(sing))
import Data.Type.Bool (If, Not, type (&&))
import Data.Type.Equality (type (==))
import Data.Vinyl.Core (Rec(..))
import Data.Vinyl.Functor qualified as Vinyl
import Data.Vinyl.Recursive (recordToList, rmap)
import Data.Vinyl.TypeLevel (type (++))
import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError)
import Prelude.Singletons (SList(..))
import Unsafe.Coerce (unsafeCoerce)

-- $setup
-- >>> import GHC.TypeLits (ErrorMessage (..))

-- | Equality constraint in form of a typeclass.
class a ~ b => IsEq a b
instance a ~ b => IsEq a b

type family IsElem (a :: k) (l :: [k]) :: Bool where
  IsElem _ '[] = 'False
  IsElem a (a ': _) = 'True
  IsElem a (_ ': as) = IsElem a as

-- | Remove all occurences of the given element.
type family (l :: [k]) / (a :: k) where
  '[] / _ = '[]
  (a ': xs) / a = xs / a
  (b ': xs) / a = b ': (xs / a)

-- | Difference between two lists.
type family (l1 :: [k]) // (l2 :: [k]) :: [k] where
  l // '[] = l
  l // (x ': xs) = (l / x) // xs

type family Guard (cond :: Bool) (a :: k) :: Maybe k where
  Guard 'False _ = 'Nothing
  Guard 'True a = 'Just a

-- | Constrain two types to be equal. If they are found not to be, produce
-- an error message. If they are shown to be equal, impose an additional
-- given constraint.
--
-- >>> :k! FailUnlessEqualElse Int Int ('Text "This should not result in a failure") ()
-- FailUnlessEqualElse Int Int ('Text "This should not result in a failure") () :: Constraint
-- = (() :: Constraint, Int ~ Int)
--
-- >>> :k! FailUnlessEqualElse Bool Int ('Text "This should result in a failure") ()
-- FailUnlessEqualElse Bool Int ('Text "This should result in a failure") () :: Constraint
-- = ((TypeError ...), Bool ~ Int)
--
-- the @~@ constraint might seem redundant, but, without it, GHC would reject
--
-- @
-- foo :: FailUnlessEqualElse a b MyError () => a -> b
-- foo = id
-- @
--
-- GHC needs to \"see\" the type equality @~@ in order to actually \"learn\"
-- something from a type family's result.
--
-- We use 'DefaultEq' here, rather than 'Data.Type.Equality.==', so this will
-- work with type variables known to be equal, even if nothing is known about
-- them concretely. For example, the following will compile:
--
-- @
-- foo :: FailUnlessEqualElse a b MyError () => a -> b
-- foo x = x
--
-- bar :: a -> a
-- bar = foo
-- @
--
-- If we used @(==)@, then bar would be rejected.
--
-- @(==)@ has its place (see the comments below it in "Data.Type.Equality")
-- but I don't think it has anything to offer us here. In particular, the equality
-- constraint we bundle up seems to win us all the reasoning power that @(==)@ would
-- provide and more. The following adaptation of the example in the
-- @Data.Type.Equality@ comments compiles:
--
-- @
-- foo :: FailUnlessEqualElse (Maybe a) (Maybe b) ('Text "yo") ()
--          :- FailUnlessEqualElse a b ('Text "heya") ()
-- foo = Sub Dict
-- @
--
-- In this example, the entire consequent follows from the equality constraint
-- in the antecedent; the `FailUnlessElsePoly` part of it is irrelevant, so we
-- don't need to be able to reason from it. If we /were/ reasoning solely using
-- @(==)@, @foo@ would be rejected because the error messages are different.
type FailUnlessEqualElse :: forall k. k -> k -> ErrorMessage -> Constraint -> Constraint
type FailUnlessEqualElse a b err els =
  ( FailUnlessElsePoly (a `DefaultEq` b) err els
  , a ~ b
  )

-- | Constrain two types to be equal, and produce an error message if
-- they are found not to be.
--
-- >>> :k! FailUnlessEqual Int Int ('Text "This should not result in a failure")
-- FailUnlessEqual Int Int ('Text "This should not result in a failure") :: Constraint
-- = (() :: Constraint, Int ~ Int)
--
-- >>> :k! FailUnlessEqual Bool Int ('Text "This should result in a failure")
-- FailUnlessEqual Bool Int ('Text "This should result in a failure") :: Constraint
-- = ((TypeError ...), Bool ~ Int)
type FailUnlessEqual :: forall k. k -> k -> ErrorMessage -> Constraint
type FailUnlessEqual a b err = FailUnlessEqualElse a b err ()

-- | An old name for 'FailUnlessEqual'.
type AssertTypesEqual :: forall k. k -> k -> ErrorMessage -> Constraint
type AssertTypesEqual a b err = FailUnlessEqual a b err

-- | A version of 'FailWhenElsePoly' that imposes an equality constraint on its
-- 'Bool' argument.
type FailWhenElse :: Bool -> ErrorMessage -> Constraint -> Constraint
type FailWhenElse cond msg els = FailUnlessEqualElse cond 'False msg els

-- | Fail with given error if the condition does not hold.
-- Otherwise, return the third argument.
--
-- There is a subtle difference between @FailWhenElsePoly@ and the
-- following type definition:
--
-- @
-- type FailWhenElsePolyAlternative cond msg els =
--   If cond
--      (TypeError msg)
--      els
-- @
--
-- If @cond@ cannot be fully reduced (e.g., it's a stuck type family
-- application or an ambiguous type) then:
--
-- * @FailWhenElsePoly@ will state that the constraint cannot be deduced (and
--   this error message will be suppressed if there are also custom type
--   errors).
--
-- * @FailWhenElsePolyAlternative@ will fail with the given error message,
--   @err@.
--
-- For example:
--
-- @
-- -- Partial function
-- type family IsZero (n :: Peano) :: Bool where
--   IsZero ('S _) = 'False
--
-- f1 :: (IsZero n ~ 'True, FailWhenElsePoly (IsZero n) ('Text "Expected zero") (() :: Constraint)) => ()
-- f1 = ()
--
-- f1 :: (IsZero n ~ 'True, FailWhenElsePolyAlternative (IsZero n) ('Text "Expected zero") (() :: Constraint)) => ()
-- f1 = ()
--
-- f1res == f1 @'Z
-- --  • Couldn't match type ‘IsZero 'Z’ with ‘'True’
--
-- f2res == f2 @'Z
-- --  • Expected zero
-- @
--
-- As you can see, the error message in @f2res@ is misleading (because the type argument
-- actually _is_ zero), so it's preferable to fail with the standard GHC error message.
type FailWhenElsePoly :: forall k. Bool -> ErrorMessage -> k -> k
type family FailWhenElsePoly cond msg els where
  FailWhenElsePoly 'True msg _els = TypeError msg
  FailWhenElsePoly 'False _ els = els

-- | A version of 'FailUnlessElsePoly' that imposes an equality constraint on its
-- 'Bool' argument.
type FailUnlessElse :: Bool -> ErrorMessage -> Constraint -> Constraint
type FailUnlessElse b msg els = FailWhenElse (Not b) msg els

-- | Fail with given error if the condition does not hold. Otherwise,
-- return the third argument.
type FailUnlessElsePoly :: forall k. Bool -> ErrorMessage -> k -> k
type FailUnlessElsePoly b e k = FailWhenElsePoly (Not b) e k

-- | Fail with given error if the condition does not hold.
type FailUnless :: Bool -> ErrorMessage -> Constraint
type FailUnless cond msg = FailUnlessElse cond msg ()

-- | Fail with given error if the condition holds.
type FailWhen :: Bool -> ErrorMessage -> Constraint
type FailWhen cond msg = FailWhenElse cond msg ()

-- | A natural conclusion from the fact that an error has not occurred.
failUnlessEvi :: forall cond msg. FailUnless cond msg :- (cond ~ 'True)
failUnlessEvi :: forall (cond :: Bool) (msg :: ErrorMessage).
FailUnless cond msg :- (cond ~ 'True)
failUnlessEvi = ((FailWhenElsePoly
    (Not (DefaultEq (Not cond) 'False)) msg (() :: Constraint),
  Not cond ~ 'False) =>
 Dict (cond ~ 'True))
-> (FailWhenElsePoly
      (Not (DefaultEq (Not cond) 'False)) msg (() :: Constraint),
    Not cond ~ 'False)
   :- (cond ~ 'True)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (FailWhenElsePoly
   (Not (DefaultEq (Not cond) 'False)) msg (() :: Constraint),
 Not cond ~ 'False) =>
Dict (cond ~ 'True)
forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint

failWhenEvi :: forall cond msg. FailWhen cond msg :- (cond ~ 'False)
failWhenEvi :: forall (cond :: Bool) (msg :: ErrorMessage).
FailWhen cond msg :- (cond ~ 'False)
failWhenEvi = ((FailWhenElsePoly
    (Not (DefaultEq cond 'False)) msg (() :: Constraint),
  cond ~ 'False) =>
 Dict (cond ~ 'False))
-> (FailWhenElsePoly
      (Not (DefaultEq cond 'False)) msg (() :: Constraint),
    cond ~ 'False)
   :- (cond ~ 'False)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (FailWhenElsePoly
   (Not (DefaultEq cond 'False)) msg (() :: Constraint),
 cond ~ 'False) =>
Dict (cond ~ 'False)
forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint

type family AllUnique (l :: [k]) :: Bool where
  AllUnique '[] = 'True
  AllUnique (x : xs) = Not (IsElem x xs) && AllUnique xs

type RequireAllUnique desc l = RequireAllUnique' desc l l

type family RequireAllUnique' (desc :: Symbol) (l :: [k]) (origL :: [k]) :: Constraint where
  RequireAllUnique' _ '[] _ = ()
  RequireAllUnique' desc (x : xs) origL =
    FailWhenElse
       (IsElem x xs)
       ('Text "Duplicated " ':<>: 'Text desc ':<>: 'Text ":" ':$$:
        'ShowType x ':$$:
        'Text "Full list: " ':<>:
        'ShowType origL
       )
       (RequireAllUnique' desc xs origL)

-- | Make sure given type is evaluated.
-- This type family fits only for types of 'Type' kind.
type family PatternMatch (a :: Type) :: Constraint where
  PatternMatch Int = ((), ())
  PatternMatch _ = ()

type family PatternMatchL (l :: [k]) :: Constraint where
  PatternMatchL '[] = ((), ())
  PatternMatchL _ = ()

-- | Bring type-level list at term-level using given function
-- to demote its individual elements.
class ReifyList (c :: k -> Constraint) (l :: [k]) where
  reifyList :: (forall a. c a => Proxy a -> r) -> [r]

instance ReifyList c '[] where
  reifyList :: forall r. (forall (a :: k). c a => Proxy a -> r) -> [r]
reifyList forall (a :: k). c a => Proxy a -> r
_ = []

instance (c x, ReifyList c xs) => ReifyList c (x ': xs) where
  reifyList :: forall r. (forall (a :: a). c a => Proxy a -> r) -> [r]
reifyList forall (a :: a). c a => Proxy a -> r
reifyElem = Proxy x -> r
forall (a :: a). c a => Proxy a -> r
reifyElem (forall {t :: a}. Proxy t
forall {k} (t :: k). Proxy t
Proxy @x) r -> [r] -> [r]
forall a. a -> [a] -> [a]
: forall k (c :: k -> Constraint) (l :: [k]) r.
ReifyList c l =>
(forall (a :: k). c a => Proxy a -> r) -> [r]
reifyList @_ @c @xs forall (a :: a). c a => Proxy a -> r
reifyElem

-- | Similar to @SingI []@, but does not require individual elements to be also
-- instance of @SingI@.
class KnownList l where
  klist :: KList l
instance KnownList '[] where
  klist :: KList '[]
klist = KList '[]
forall k. KList '[]
KNil
instance KnownList xs => KnownList (x ': xs) where
  klist :: KList (x : xs)
klist = Proxy x -> Proxy xs -> KList (x : xs)
forall {k} (xs :: [k]) (x :: k).
KnownList xs =>
Proxy x -> Proxy xs -> KList (x : xs)
KCons Proxy x
forall {k} (t :: k). Proxy t
Proxy Proxy xs
forall {k} (t :: k). Proxy t
Proxy

-- | Given a type-level list that is 'SingI', construct evidence that it is also
-- a 'KnownList'. Note that 'KnownList' is weaker, hence this construction
-- is always possible.
knownListFromSingI :: forall xs. SingI xs => Dict (KnownList xs)
knownListFromSingI :: forall {k} (xs :: [k]). SingI xs => Dict (KnownList xs)
knownListFromSingI = SList xs -> Dict (KnownList xs)
forall {k} (ys :: [k]). SList ys -> Dict (KnownList ys)
go (forall (a :: [k]). SingI a => Sing a
forall {k} (a :: k). SingI a => Sing a
sing @xs)
  where
    go :: forall ys. SList ys -> Dict (KnownList ys)
    go :: forall {k} (ys :: [k]). SList ys -> Dict (KnownList ys)
go = \case
      SList ys
SNil -> Dict (KnownList ys)
forall (a :: Constraint). a => Dict a
Dict
      SCons Sing n1
_ Sing n2
ys -> KnownList n2 => Dict (KnownList ys)
forall (a :: Constraint). a => Dict a
Dict (KnownList n2 => Dict (KnownList ys))
-> Dict (KnownList n2) -> Dict (KnownList ys)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SList n2 -> Dict (KnownList n2)
forall {k} (ys :: [k]). SList ys -> Dict (KnownList ys)
go Sing n2
SList n2
ys

-- | @Data.List.Singletons.SList@ analogue for 'KnownList'.
data KList (l :: [k]) where
  KNil :: KList '[]
  KCons :: KnownList xs => Proxy x -> Proxy xs -> KList (x ': xs)

type RSplit l r = KnownList l

-- | Split a record into two pieces.
rsplit
  :: forall k (l :: [k]) (r :: [k]) f.
      (RSplit l r)
  => Rec f (l ++ r) -> (Rec f l, Rec f r)
rsplit :: forall k (l :: [k]) (r :: [k]) (f :: k -> *).
RSplit l r =>
Rec f (l ++ r) -> (Rec f l, Rec f r)
rsplit = case forall (l :: [k]). KnownList l => KList l
forall {k} (l :: [k]). KnownList l => KList l
klist @l of
  KList l
KNil -> (Rec f '[]
forall {u} (a :: u -> *). Rec a '[]
RNil, )
  KCons{} -> \(f r
x :& Rec f rs
r) ->
    let (Rec f xs
x1, Rec f r
r1) = Rec f (xs ++ r) -> (Rec f xs, Rec f r)
forall k (l :: [k]) (r :: [k]) (f :: k -> *).
RSplit l r =>
Rec f (l ++ r) -> (Rec f l, Rec f r)
rsplit Rec f rs
Rec f (xs ++ r)
r
    in (f r
x f r -> Rec f xs -> Rec f (r : xs)
forall {u} (a :: u -> *) (r :: u) (rs :: [u]).
a r -> Rec a rs -> Rec a (r : rs)
:& Rec f xs
x1, Rec f r
r1)

-- | A value of type parametrized with /some/ type parameter.
data Some1 (f :: k -> Type) =
  forall a. Some1 (f a)

deriving stock instance (forall a. Show (f a)) => Show (Some1 f)

recordToSomeList :: Rec f l -> [Some1 f]
recordToSomeList :: forall {k} (f :: k -> *) (l :: [k]). Rec f l -> [Some1 f]
recordToSomeList = Rec (Const (Some1 f)) l -> [Some1 f]
forall {u} a (rs :: [u]). Rec (Const a) rs -> [a]
recordToList (Rec (Const (Some1 f)) l -> [Some1 f])
-> (Rec f l -> Rec (Const (Some1 f)) l) -> Rec f l -> [Some1 f]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (x :: k). f x -> Const (Some1 f) x)
-> Rec f l -> Rec (Const (Some1 f)) l
forall {u} (f :: u -> *) (g :: u -> *) (rs :: [u]).
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (Some1 f -> Const (Some1 f) x
forall k a (b :: k). a -> Const a b
Vinyl.Const (Some1 f -> Const (Some1 f) x)
-> (f x -> Some1 f) -> f x -> Const (Some1 f) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> Some1 f
forall k (f :: k -> *) (a :: k). f a -> Some1 f
Some1)

type ConcatListOfTypesAssociativity a b c = ((a ++ b) ++ c) ~ (a ++ (b ++ c))

-- | GHC can't deduce this itself because
-- in general a type family might be not associative,
-- what brings extra difficulties and redundant constraints,
-- especially if you have complex types.
-- But (++) type family is associative, so let's define this small hack.
listOfTypesConcatAssociativityAxiom :: forall a b c . Dict (ConcatListOfTypesAssociativity a b c)
listOfTypesConcatAssociativityAxiom :: forall {k} (a :: [k]) (b :: [k]) (c :: [k]).
Dict (ConcatListOfTypesAssociativity a b c)
listOfTypesConcatAssociativityAxiom = Dict (((a ++ b) ++ c) ~ (a ++ (b ++ c)))
forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint

-- | Constaints that can be provided on demand.
--
-- Needless to say, this is a pretty unsafe operation. This typeclass makes
-- using it safer in a sense that getting a segfault becomes harder, but still
-- it deceives the type system and should be used only if providing a proper
-- proof would be too difficult.
class MockableConstraint (c :: Constraint) where
  -- | Produce a constraint out of thin air.
  unsafeProvideConstraint :: Dict c

instance MockableConstraint (a ~ b) where
  unsafeProvideConstraint :: Dict (a ~ b)
unsafeProvideConstraint = Dict (Int ~ Int) -> Dict (a ~ b)
forall a b. a -> b
unsafeCoerce (Dict (Int ~ Int) -> Dict (a ~ b))
-> Dict (Int ~ Int) -> Dict (a ~ b)
forall a b. (a -> b) -> a -> b
$ forall (a :: Constraint). a => Dict a
Dict @(Int ~ Int)

-- | In majority of the cases we don't want to mock typeclass constraints
-- since coercing instances of typeclasses with methods is utterly unsafe.
instance {-# OVERLAPPABLE #-} c a => MockableConstraint (c a) where
  unsafeProvideConstraint :: Dict (c a)
unsafeProvideConstraint = Dict (c a)
forall (a :: Constraint). a => Dict a
Dict

instance ( MockableConstraint c1
         , MockableConstraint c2
         ) => MockableConstraint (c1, c2) where
  unsafeProvideConstraint :: Dict (c1, c2)
unsafeProvideConstraint = Identity (Dict (c1, c2)) -> Dict (c1, c2)
forall a. Identity a -> a
runIdentity (Identity (Dict (c1, c2)) -> Dict (c1, c2))
-> Identity (Dict (c1, c2)) -> Dict (c1, c2)
forall a b. (a -> b) -> a -> b
$ do
    Dict c1
Dict <- Dict c1 -> Identity (Dict c1)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict c1 -> Identity (Dict c1)) -> Dict c1 -> Identity (Dict c1)
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @c1
    Dict c2
Dict <- Dict c2 -> Identity (Dict c2)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict c2 -> Identity (Dict c2)) -> Dict c2 -> Identity (Dict c2)
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @c2
    Dict (c1, c2) -> Identity (Dict (c1, c2))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (c1, c2)
forall (a :: Constraint). a => Dict a
Dict
  {-# INLINE unsafeProvideConstraint #-}

instance ( MockableConstraint c1
         , MockableConstraint c2
         , MockableConstraint c3
         ) => MockableConstraint (c1, c2, c3) where
  unsafeProvideConstraint :: Dict (c1, c2, c3)
unsafeProvideConstraint = Identity (Dict (c1, c2, c3)) -> Dict (c1, c2, c3)
forall a. Identity a -> a
runIdentity (Identity (Dict (c1, c2, c3)) -> Dict (c1, c2, c3))
-> Identity (Dict (c1, c2, c3)) -> Dict (c1, c2, c3)
forall a b. (a -> b) -> a -> b
$ do
    Dict (c1, c2)
Dict <- Dict (c1, c2) -> Identity (Dict (c1, c2))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict (c1, c2) -> Identity (Dict (c1, c2)))
-> Dict (c1, c2) -> Identity (Dict (c1, c2))
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @(c1, c2)
    Dict c3
Dict <- Dict c3 -> Identity (Dict c3)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict c3 -> Identity (Dict c3)) -> Dict c3 -> Identity (Dict c3)
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @c3
    Dict (c1, c2, c3) -> Identity (Dict (c1, c2, c3))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (c1, c2, c3)
forall (a :: Constraint). a => Dict a
Dict
  {-# INLINE unsafeProvideConstraint #-}

instance ( MockableConstraint c1
         , MockableConstraint c2
         , MockableConstraint c3
         , MockableConstraint c4
         ) => MockableConstraint (c1, c2, c3, c4) where
  unsafeProvideConstraint :: Dict (c1, c2, c3, c4)
unsafeProvideConstraint = Identity (Dict (c1, c2, c3, c4)) -> Dict (c1, c2, c3, c4)
forall a. Identity a -> a
runIdentity (Identity (Dict (c1, c2, c3, c4)) -> Dict (c1, c2, c3, c4))
-> Identity (Dict (c1, c2, c3, c4)) -> Dict (c1, c2, c3, c4)
forall a b. (a -> b) -> a -> b
$ do
    Dict (c1, c2, c3)
Dict <- Dict (c1, c2, c3) -> Identity (Dict (c1, c2, c3))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict (c1, c2, c3) -> Identity (Dict (c1, c2, c3)))
-> Dict (c1, c2, c3) -> Identity (Dict (c1, c2, c3))
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @(c1, c2, c3)
    Dict c4
Dict <- Dict c4 -> Identity (Dict c4)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict c4 -> Identity (Dict c4)) -> Dict c4 -> Identity (Dict c4)
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @c4
    Dict (c1, c2, c3, c4) -> Identity (Dict (c1, c2, c3, c4))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (c1, c2, c3, c4)
forall (a :: Constraint). a => Dict a
Dict
  {-# INLINE unsafeProvideConstraint #-}

instance ( MockableConstraint c1
         , MockableConstraint c2
         , MockableConstraint c3
         , MockableConstraint c4
         , MockableConstraint c5
         ) => MockableConstraint (c1, c2, c3, c4, c5) where
  unsafeProvideConstraint :: Dict (c1, c2, c3, c4, c5)
unsafeProvideConstraint = Identity (Dict (c1, c2, c3, c4, c5)) -> Dict (c1, c2, c3, c4, c5)
forall a. Identity a -> a
runIdentity (Identity (Dict (c1, c2, c3, c4, c5)) -> Dict (c1, c2, c3, c4, c5))
-> Identity (Dict (c1, c2, c3, c4, c5))
-> Dict (c1, c2, c3, c4, c5)
forall a b. (a -> b) -> a -> b
$ do
    Dict (c1, c2, c3, c4)
Dict <- Dict (c1, c2, c3, c4) -> Identity (Dict (c1, c2, c3, c4))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict (c1, c2, c3, c4) -> Identity (Dict (c1, c2, c3, c4)))
-> Dict (c1, c2, c3, c4) -> Identity (Dict (c1, c2, c3, c4))
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @(c1, c2, c3, c4)
    Dict c5
Dict <- Dict c5 -> Identity (Dict c5)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Dict c5 -> Identity (Dict c5)) -> Dict c5 -> Identity (Dict c5)
forall a b. (a -> b) -> a -> b
$ forall (c :: Constraint). MockableConstraint c => Dict c
unsafeProvideConstraint @c5
    Dict (c1, c2, c3, c4, c5) -> Identity (Dict (c1, c2, c3, c4, c5))
forall (m :: * -> *) a. Monad m => a -> m a
return Dict (c1, c2, c3, c4, c5)
forall (a :: Constraint). a => Dict a
Dict
  {-# INLINE unsafeProvideConstraint #-}

-- | Utility function to help transform the first argument of a binfunctor.
onFirst :: Bifunctor p => p a c -> (a -> b) -> p b c
onFirst :: forall (p :: * -> * -> *) a c b.
Bifunctor p =>
p a c -> (a -> b) -> p b c
onFirst = ((a -> b) -> p a c -> p b c) -> p a c -> (a -> b) -> p b c
forall a b c. (a -> b -> c) -> b -> a -> c
flip (a -> b) -> p a c -> p b c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first