{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Row.Dictionaries
--
-- This module exports various dictionaries that help the type-checker when
-- dealing with row-types.
--
-- For the various axioms, type variables are consistently in the following order:
--
--  * Any types that do not belong later.
--
--  * Labels
--
--  * Row-types
--
--      * If applicable, the type in the row-type at the given label goes after
--      each row-type
--
--  * Constraints
-----------------------------------------------------------------------------


module Data.Row.Dictionaries
  ( -- * Axioms
    uniqueMap, uniqueAp, uniqueApSingle, uniqueZip
  , extendHas, mapHas, apHas, apSingleHas
  , mapExtendSwap, apExtendSwap, apSingleExtendSwap, zipExtendSwap
  , mapMinJoin, apSingleMinJoin
  , FreeForall
  , FreeBiForall
  , freeForall
  , mapForall
  , apSingleForall
  , subsetJoin, subsetJoin', subsetRestrict, subsetTrans
  , mapDifference, apSingleDifference
  -- ** Helper Types
  , IsA(..)
  , As(..)
  , ActsOn(..)
  , As'(..)
  -- * Re-exports
  , Dict(..), (:-)(..), HasDict(..), (\\), withDict
  , Unconstrained, Unconstrained1, Unconstrained2

  )
where

import Data.Constraint
import Data.Functor.Const
import Data.Proxy
import qualified Unsafe.Coerce as UNSAFE
import GHC.TypeLits

import Data.Row.Internal



-- | This data type is used to for its ability to existentially bind a type
-- variable.  Particularly, it says that for the type 'a', there exists a 't'
-- such that @a ~ f t@ and @c t@ holds.
data As c f a where
  As :: forall c f a t. (a ~ f t, c t) => As c f a

-- | A class to capture the idea of 'As' so that it can be partially applied in
-- a context.
class IsA c f a where
  as :: As c f a

instance c a => IsA c f (f a) where
  as :: As c f (f a)
as = As c f (f a)
forall k k (c :: k -> Constraint) (f :: k -> k) (a :: k) (t :: k).
(a ~ f t, c t) =>
As c f a
As

-- | Like 'As', but here we know the underlying value is some 'f' applied to the
-- given type 'a'.
data As' c t a where
  As' :: forall c f a t. (a ~ f t, c f) => As' c t a

-- | A class to capture the idea of 'As'' so that it can be partially applied in
-- a context.
class ActsOn c t a where
  actsOn :: As' c t a

instance c f => ActsOn c t (f t) where
  actsOn :: As' c t (f t)
actsOn = As' c t (f t)
forall k k (c :: (k -> k) -> Constraint) (f :: k -> k) (a :: k)
       (t :: k).
(a ~ f t, c f) =>
As' c t a
As'

-- | An internal type used by the 'metamorph' in 'mapForall'.
newtype MapForall c f (r :: Row k) = MapForall { MapForall c f r -> Dict (Forall (Map f r) (IsA c f))
unMapForall :: Dict (Forall (Map f r) (IsA c f)) }

-- | An internal type used by the 'metamorph' in 'apSingleForall'.
newtype ApSingleForall c a (fs :: Row (k -> k')) = ApSingleForall
  { ApSingleForall c a fs -> Dict (Forall (ApSingle fs a) (ActsOn c a))
unApSingleForall :: Dict (Forall (ApSingle fs a) (ActsOn c a)) }

-- | This allows us to derive a @Forall (Map f r) ..@ from a @Forall r ..@.
mapForall :: forall f ρ c. Forall ρ c :- Forall (Map f ρ) (IsA c f)
mapForall :: Forall ρ c :- Forall (Map f ρ) (IsA c f)
mapForall = (Forall ρ c => Dict (Forall (Map f ρ) (IsA c f)))
-> Forall ρ c :- Forall (Map f ρ) (IsA c f)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((Forall ρ c => Dict (Forall (Map f ρ) (IsA c f)))
 -> Forall ρ c :- Forall (Map f ρ) (IsA c f))
-> (Forall ρ c => Dict (Forall (Map f ρ) (IsA c f)))
-> Forall ρ c :- Forall (Map f ρ) (IsA c f)
forall a b. (a -> b) -> a -> b
$ MapForall c f ρ -> Dict (Forall (Map f ρ) (IsA c f))
forall k (c :: k -> Constraint) k (f :: k -> k) (r :: Row k).
MapForall c f r -> Dict (Forall (Map f r) (IsA c f))
unMapForall (MapForall c f ρ -> Dict (Forall (Map f ρ) (IsA c f)))
-> MapForall c f ρ -> Dict (Forall (Map f ρ) (IsA c f))
forall a b. (a -> b) -> a -> b
$ Proxy (Proxy Proxy, Proxy Const)
-> (Proxy Empty -> MapForall c f Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> Proxy ρ -> Const (Proxy (ρ .- ℓ)) (Proxy τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> Const (MapForall c f ρ) (Proxy τ)
    -> MapForall c f (Extend ℓ τ ρ))
-> Proxy ρ
-> MapForall c f ρ
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @ρ @c @Const @Proxy @(MapForall c f) @Proxy Proxy (Proxy Proxy, Proxy Const)
forall k (t :: k). Proxy t
Proxy Proxy Empty -> MapForall c f Empty
forall k k (f :: k -> k) (r :: Row k) (c :: k -> Constraint) p.
Forall (Map f r) (IsA c f) =>
p -> MapForall c f r
empty forall k k p p (t :: k) (b :: k). p -> p -> Const (Proxy t) b
forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> Proxy ρ -> Const (Proxy (ρ .- ℓ)) (Proxy τ)
uncons forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Const (MapForall c f ρ) (Proxy τ)
-> MapForall c f (Extend ℓ τ ρ)
cons (Proxy ρ -> MapForall c f ρ) -> Proxy ρ -> MapForall c f ρ
forall a b. (a -> b) -> a -> b
$ Proxy ρ
forall k (t :: k). Proxy t
Proxy
  where empty :: p -> MapForall c f r
empty p
_ = Dict (Forall (Map f r) (IsA c f)) -> MapForall c f r
forall k k (c :: k -> Constraint) (f :: k -> k) (r :: Row k).
Dict (Forall (Map f r) (IsA c f)) -> MapForall c f r
MapForall Dict (Forall (Map f r) (IsA c f))
forall (a :: Constraint). a => Dict a
Dict
        uncons :: p -> p -> Const (Proxy t) b
uncons p
_ p
_ = Proxy t -> Const (Proxy t) b
forall k a (b :: k). a -> Const a b
Const Proxy t
forall k (t :: k). Proxy t
Proxy
        cons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ))
             => Label ℓ -> Const (MapForall c f ρ) (Proxy τ)
             -> MapForall c f (Extend ℓ τ ρ)
        cons :: Label ℓ
-> Const (MapForall c f ρ) (Proxy τ)
-> MapForall c f (Extend ℓ τ ρ)
cons Label ℓ
_ (Const (MapForall Dict (Forall (Map f ρ) (IsA c f))
Dict)) = case FrontExtends ℓ τ ρ => FrontExtendsDict ℓ τ ρ
forall k (l :: Symbol) (t :: k) (r :: Row k).
FrontExtends l t r =>
FrontExtendsDict l t r
frontExtendsDict @ℓ @τ @ρ of
          FrontExtendsDict Dict
  (ρ ~ 'R ρ, 'R ((ℓ ':-> τ) : ρ) ≈ Extend ℓ τ ('R ρ),
   AllUniqueLabelsR ((ℓ ':-> τ) : ρ))
Dict -> Dict (Forall (Map f ('R ((ℓ ':-> τ) : ρ))) (IsA c f))
-> MapForall c f ('R ((ℓ ':-> τ) : ρ))
forall k k (c :: k -> Constraint) (f :: k -> k) (r :: Row k).
Dict (Forall (Map f r) (IsA c f)) -> MapForall c f r
MapForall Dict (Forall (Map f ('R ((ℓ ':-> τ) : ρ))) (IsA c f))
forall (a :: Constraint). a => Dict a
Dict
            ((Extend ℓ (f τ) ('R (MapR f ρ)) ~ 'R ((ℓ ':-> f τ) : MapR f ρ)) =>
 MapForall c f ('R ((ℓ ':-> τ) : ρ)))
-> Dict
     (Extend ℓ (f τ) ('R (MapR f ρ)) ~ 'R ((ℓ ':-> f τ) : MapR f ρ))
-> MapForall c f ('R ((ℓ ':-> τ) : ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (f τ) (Map f ρ) ≈ Map f (Extend ℓ τ ρ))
forall k b (f :: k -> b) (ℓ :: Symbol) (τ :: k) (r :: Row k).
Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap @f @ℓ @τ @ρ
            ((AllUniqueLabelsR ((ℓ ':-> f τ) : MapR f ρ)
  ~ AllUniqueLabels (Extend ℓ τ ρ)) =>
 MapForall c f ('R ((ℓ ':-> τ) : ρ)))
-> Dict
     (AllUniqueLabelsR ((ℓ ':-> f τ) : MapR f ρ)
      ~ AllUniqueLabels (Extend ℓ τ ρ))
-> MapForall c f ('R ((ℓ ':-> τ) : ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (AllUniqueLabels (Map f (Extend ℓ τ ρ))
   ≈ AllUniqueLabels (Extend ℓ τ ρ))
forall k k (f :: k -> k) (r :: Row k).
Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
uniqueMap @f @(Extend ℓ τ ρ)

-- | This allows us to derive a @Forall (ApSingle f r) ..@ from a @Forall f ..@.
apSingleForall :: forall a fs c. Forall fs c :- Forall (ApSingle fs a) (ActsOn c a)
apSingleForall :: Forall fs c :- Forall (ApSingle fs a) (ActsOn c a)
apSingleForall = (Forall fs c => Dict (Forall (ApSingle fs a) (ActsOn c a)))
-> Forall fs c :- Forall (ApSingle fs a) (ActsOn c a)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((Forall fs c => Dict (Forall (ApSingle fs a) (ActsOn c a)))
 -> Forall fs c :- Forall (ApSingle fs a) (ActsOn c a))
-> (Forall fs c => Dict (Forall (ApSingle fs a) (ActsOn c a)))
-> Forall fs c :- Forall (ApSingle fs a) (ActsOn c a)
forall a b. (a -> b) -> a -> b
$ ApSingleForall c a fs -> Dict (Forall (ApSingle fs a) (ActsOn c a))
forall k k' (c :: (k -> k') -> Constraint) (a :: k)
       (fs :: Row (k -> k')).
ApSingleForall c a fs -> Dict (Forall (ApSingle fs a) (ActsOn c a))
unApSingleForall (ApSingleForall c a fs
 -> Dict (Forall (ApSingle fs a) (ActsOn c a)))
-> ApSingleForall c a fs
-> Dict (Forall (ApSingle fs a) (ActsOn c a))
forall a b. (a -> b) -> a -> b
$ Proxy (Proxy Proxy, Proxy Const)
-> (Proxy Empty -> ApSingleForall c a Empty)
-> (forall (ℓ :: Symbol) (τ :: k -> k) (ρ :: Row (k -> k)).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> Proxy ρ -> Const (Proxy (ρ .- ℓ)) (Proxy τ))
-> (forall (ℓ :: Symbol) (τ :: k -> k) (ρ :: Row (k -> k)).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ
    -> Const (ApSingleForall c a ρ) (Proxy τ)
    -> ApSingleForall c a (Extend ℓ τ ρ))
-> Proxy fs
-> ApSingleForall c a fs
forall k (r :: Row k) (c :: k -> Constraint) (p :: * -> * -> *)
       (f :: Row k -> *) (g :: Row k -> *) (h :: k -> *).
(Forall r c, Bifunctor p) =>
Proxy (Proxy h, Proxy p)
-> (f Empty -> g Empty)
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
    Label ℓ -> f ρ -> p (f (ρ .- ℓ)) (h τ))
-> (forall (ℓ :: Symbol) (τ :: k) (ρ :: Row k).
    (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
     AllUniqueLabels (Extend ℓ τ ρ)) =>
    Label ℓ -> p (g ρ) (h τ) -> g (Extend ℓ τ ρ))
-> f r
-> g r
metamorph @_ @fs @c @Const @Proxy @(ApSingleForall c a) @Proxy Proxy (Proxy Proxy, Proxy Const)
forall k (t :: k). Proxy t
Proxy Proxy Empty -> ApSingleForall c a Empty
forall k k' (fs :: Row (k -> k')) (a :: k)
       (c :: (k -> k') -> Constraint) p.
Forall (ApSingle fs a) (ActsOn c a) =>
p -> ApSingleForall c a fs
empty forall k k p p (t :: k) (b :: k). p -> p -> Const (Proxy t) b
forall (ℓ :: Symbol) (τ :: k -> k) (ρ :: Row (k -> k)).
(KnownSymbol ℓ, c τ, HasType ℓ τ ρ) =>
Label ℓ -> Proxy ρ -> Const (Proxy (ρ .- ℓ)) (Proxy τ)
uncons forall (ℓ :: Symbol) (τ :: k -> k) (ρ :: Row (k -> k)).
(KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ,
 AllUniqueLabels (Extend ℓ τ ρ)) =>
Label ℓ
-> Const (ApSingleForall c a ρ) (Proxy τ)
-> ApSingleForall c a (Extend ℓ τ ρ)
cons (Proxy fs -> ApSingleForall c a fs)
-> Proxy fs -> ApSingleForall c a fs
forall a b. (a -> b) -> a -> b
$ Proxy fs
forall k (t :: k). Proxy t
Proxy
  where empty :: p -> ApSingleForall c a fs
empty p
_ = Dict (Forall (ApSingle fs a) (ActsOn c a)) -> ApSingleForall c a fs
forall k k' (c :: (k -> k') -> Constraint) (a :: k)
       (fs :: Row (k -> k')).
Dict (Forall (ApSingle fs a) (ActsOn c a)) -> ApSingleForall c a fs
ApSingleForall Dict (Forall (ApSingle fs a) (ActsOn c a))
forall (a :: Constraint). a => Dict a
Dict
        uncons :: p -> p -> Const (Proxy t) b
uncons p
_ p
_ = Proxy t -> Const (Proxy t) b
forall k a (b :: k). a -> Const a b
Const Proxy t
forall k (t :: k). Proxy t
Proxy
        cons :: forall ℓ τ ρ. (KnownSymbol ℓ, c τ, FrontExtends ℓ τ ρ, AllUniqueLabels (Extend ℓ τ ρ))
             => Label ℓ -> Const (ApSingleForall c a ρ) (Proxy τ)
             -> ApSingleForall c a (Extend ℓ τ ρ)
        cons :: Label ℓ
-> Const (ApSingleForall c a ρ) (Proxy τ)
-> ApSingleForall c a (Extend ℓ τ ρ)
cons Label ℓ
_ (Const (ApSingleForall Dict (Forall (ApSingle ρ a) (ActsOn c a))
Dict)) = case FrontExtends ℓ τ ρ => FrontExtendsDict ℓ τ ρ
forall k (l :: Symbol) (t :: k) (r :: Row k).
FrontExtends l t r =>
FrontExtendsDict l t r
frontExtendsDict @ℓ @τ @ρ of
          FrontExtendsDict Dict
  (ρ ~ 'R ρ, 'R ((ℓ ':-> τ) : ρ) ≈ Extend ℓ τ ('R ρ),
   AllUniqueLabelsR ((ℓ ':-> τ) : ρ))
Dict -> Dict (Forall (ApSingle ('R ((ℓ ':-> τ) : ρ)) a) (ActsOn c a))
-> ApSingleForall c a ('R ((ℓ ':-> τ) : ρ))
forall k k' (c :: (k -> k') -> Constraint) (a :: k)
       (fs :: Row (k -> k')).
Dict (Forall (ApSingle fs a) (ActsOn c a)) -> ApSingleForall c a fs
ApSingleForall Dict (Forall (ApSingle ('R ((ℓ ':-> τ) : ρ)) a) (ActsOn c a))
forall (a :: Constraint). a => Dict a
Dict
            ((Extend ℓ (τ a) ('R (ApSingleR ρ a))
  ~ 'R ((ℓ ':-> τ a) : ApSingleR ρ a)) =>
 ApSingleForall c a ('R ((ℓ ':-> τ) : ρ)))
-> Dict
     (Extend ℓ (τ a) ('R (ApSingleR ρ a))
      ~ 'R ((ℓ ':-> τ a) : ApSingleR ρ a))
-> ApSingleForall c a ('R ((ℓ ':-> τ) : ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict (Extend ℓ (τ a) (ApSingle ρ a) ≈ ApSingle (Extend ℓ τ ρ) a)
forall a b (τ :: a) (ℓ :: Symbol) (f :: a -> b)
       (r :: Row (a -> b)).
Dict (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ)
apSingleExtendSwap @a @ℓ @τ @ρ
            ((AllUniqueLabelsR ((ℓ ':-> τ a) : ApSingleR ρ a)
  ~ AllUniqueLabels (Extend ℓ τ ρ)) =>
 ApSingleForall c a ('R ((ℓ ':-> τ) : ρ)))
-> Dict
     (AllUniqueLabelsR ((ℓ ':-> τ a) : ApSingleR ρ a)
      ~ AllUniqueLabels (Extend ℓ τ ρ))
-> ApSingleForall c a ('R ((ℓ ':-> τ) : ρ))
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ Dict
  (AllUniqueLabels (ApSingle (Extend ℓ τ ρ) a)
   ≈ AllUniqueLabels (Extend ℓ τ ρ))
forall a k (x :: a) (r :: Row (a -> k)).
Dict (AllUniqueLabels (ApSingle r x) ≈ AllUniqueLabels r)
uniqueApSingle @a @(Extend ℓ τ ρ)

-- | Allow any 'Forall' over a row-type, be usable for 'Unconstrained1'.
freeForall :: forall r c. Forall r c :- Forall r Unconstrained1
freeForall :: Forall r c :- Forall r Unconstrained1
freeForall = (Forall r c => Dict (Forall r Unconstrained1))
-> Forall r c :- Forall r Unconstrained1
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((Forall r c => Dict (Forall r Unconstrained1))
 -> Forall r c :- Forall r Unconstrained1)
-> (Forall r c => Dict (Forall r Unconstrained1))
-> Forall r c :- Forall r Unconstrained1
forall a b. (a -> b) -> a -> b
$ Dict (Forall r c) -> Dict (Forall r Unconstrained1)
forall a b. a -> b
UNSAFE.unsafeCoerce @(Dict (Forall r c)) Dict (Forall r c)
forall (a :: Constraint). a => Dict a
Dict

-- | `FreeForall` can be used when a `Forall` constraint is necessary but there
-- is no particular constraint we care about.
type FreeForall r = Forall r Unconstrained1

-- | `FreeForall` can be used when a `BiForall` constraint is necessary but
-- there is no particular constraint we care about.
type FreeBiForall r1 r2 = BiForall r1 r2 Unconstrained2

-- | If we know that 'r' has been extended with @l .== t@, then we know that this
-- extension at the label 'l' must be 't'.
extendHas :: forall l t r. Dict (Extend l t r .! l ≈ t)
extendHas :: Dict ((Extend l t r .! l) ≈ t)
extendHas = Dict Unconstrained -> Dict ((Extend l t r .! l) ≈ t)
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained -> Dict ((Extend l t r .! l) ≈ t))
-> Dict Unconstrained -> Dict ((Extend l t r .! l) ≈ t)
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | This allows us to derive @Map f r .! l ≈ f t@ from @r .! l ≈ t@
mapHas :: forall f l t r. (r .! l ≈ t) :- (Map f r .! l ≈ f t, Map f r .- l ≈ Map f (r .- l))
mapHas :: ((r .! l) ≈ t)
:- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
mapHas = (((r .! l) ≈ t) =>
 Dict ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l)))
-> ((r .! l) ≈ t)
   :- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((((r .! l) ≈ t) =>
  Dict ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l)))
 -> ((r .! l) ≈ t)
    :- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l)))
-> (((r .! l) ≈ t) =>
    Dict ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l)))
-> ((r .! l) ≈ t)
   :- ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
forall a b. (a -> b) -> a -> b
$ Dict (Unconstrained, Unconstrained)
-> Dict ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict (Unconstrained, Unconstrained)
 -> Dict ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l)))
-> Dict (Unconstrained, Unconstrained)
-> Dict ((Map f r .! l) ≈ f t, (Map f r .- l) ≈ Map f (r .- l))
forall a b. (a -> b) -> a -> b
$ (Unconstrained, Unconstrained) =>
Dict (Unconstrained, Unconstrained)
forall (a :: Constraint). a => Dict a
Dict @(Unconstrained, Unconstrained)

-- | This allows us to derive @Ap ϕ ρ .! l ≈ f t@ from @ϕ .! l ≈ f@ and @ρ .! l ≈ t@
apHas :: forall l f ϕ t ρ. (ϕ .! l ≈ f, ρ .! l ≈ t) :- (Ap ϕ ρ .! l ≈ f t, Ap ϕ ρ .- l ≈ Ap (ϕ .- l) (ρ .- l))
apHas :: ((ϕ .! l) ≈ f, (ρ .! l) ≈ t)
:- ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l))
apHas = (((ϕ .! l) ≈ f, (ρ .! l) ≈ t) =>
 Dict ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l)))
-> ((ϕ .! l) ≈ f, (ρ .! l) ≈ t)
   :- ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l))
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((((ϕ .! l) ≈ f, (ρ .! l) ≈ t) =>
  Dict ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l)))
 -> ((ϕ .! l) ≈ f, (ρ .! l) ≈ t)
    :- ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l)))
-> (((ϕ .! l) ≈ f, (ρ .! l) ≈ t) =>
    Dict ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l)))
-> ((ϕ .! l) ≈ f, (ρ .! l) ≈ t)
   :- ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l))
forall a b. (a -> b) -> a -> b
$ Dict (Unconstrained, Unconstrained)
-> Dict ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l))
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict (Unconstrained, Unconstrained)
 -> Dict
      ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l)))
-> Dict (Unconstrained, Unconstrained)
-> Dict ((Ap ϕ ρ .! l) ≈ f t, (Ap ϕ ρ .- l) ≈ Ap (ϕ .- l) (ρ .- l))
forall a b. (a -> b) -> a -> b
$ (Unconstrained, Unconstrained) =>
Dict (Unconstrained, Unconstrained)
forall (a :: Constraint). a => Dict a
Dict @(Unconstrained, Unconstrained)

-- | This allows us to derive @ApSingle r x .! l ≈ f x@ from @r .! l ≈ f@
apSingleHas :: forall x l f r. (r .! l ≈ f) :- (ApSingle r x .! l ≈ f x, ApSingle r x .- l ≈ ApSingle (r .- l) x)
apSingleHas :: ((r .! l) ≈ f)
:- ((ApSingle r x .! l) ≈ f x,
    (ApSingle r x .- l) ≈ ApSingle (r .- l) x)
apSingleHas = (((r .! l) ≈ f) =>
 Dict
   ((ApSingle r x .! l) ≈ f x,
    (ApSingle r x .- l) ≈ ApSingle (r .- l) x))
-> ((r .! l) ≈ f)
   :- ((ApSingle r x .! l) ≈ f x,
       (ApSingle r x .- l) ≈ ApSingle (r .- l) x)
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((((r .! l) ≈ f) =>
  Dict
    ((ApSingle r x .! l) ≈ f x,
     (ApSingle r x .- l) ≈ ApSingle (r .- l) x))
 -> ((r .! l) ≈ f)
    :- ((ApSingle r x .! l) ≈ f x,
        (ApSingle r x .- l) ≈ ApSingle (r .- l) x))
-> (((r .! l) ≈ f) =>
    Dict
      ((ApSingle r x .! l) ≈ f x,
       (ApSingle r x .- l) ≈ ApSingle (r .- l) x))
-> ((r .! l) ≈ f)
   :- ((ApSingle r x .! l) ≈ f x,
       (ApSingle r x .- l) ≈ ApSingle (r .- l) x)
forall a b. (a -> b) -> a -> b
$ Dict (Unconstrained, Unconstrained)
-> Dict
     ((ApSingle r x .! l) ≈ f x,
      (ApSingle r x .- l) ≈ ApSingle (r .- l) x)
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict (Unconstrained, Unconstrained)
 -> Dict
      ((ApSingle r x .! l) ≈ f x,
       (ApSingle r x .- l) ≈ ApSingle (r .- l) x))
-> Dict (Unconstrained, Unconstrained)
-> Dict
     ((ApSingle r x .! l) ≈ f x,
      (ApSingle r x .- l) ≈ ApSingle (r .- l) x)
forall a b. (a -> b) -> a -> b
$ (Unconstrained, Unconstrained) =>
Dict (Unconstrained, Unconstrained)
forall (a :: Constraint). a => Dict a
Dict @(Unconstrained, Unconstrained)

-- | Proof that the 'Map' type family preserves labels and their ordering.
mapExtendSwap :: forall f ℓ τ r. Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap :: Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
mapExtendSwap = Dict Unconstrained
-> Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r)))
-> Dict Unconstrained
-> Dict (Extend ℓ (f τ) (Map f r) ≈ Map f (Extend ℓ τ r))
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | Proof that the 'Ap' type family preserves labels and their ordering.
apExtendSwap :: forall ℓ f fs τ r. Dict (Extend ℓ (f τ) (Ap fs r) ≈ Ap (Extend ℓ f fs) (Extend ℓ τ r))
apExtendSwap :: Dict (Extend ℓ (f τ) (Ap fs r) ≈ Ap (Extend ℓ f fs) (Extend ℓ τ r))
apExtendSwap = Dict Unconstrained
-> Dict
     (Extend ℓ (f τ) (Ap fs r) ≈ Ap (Extend ℓ f fs) (Extend ℓ τ r))
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict
      (Extend ℓ (f τ) (Ap fs r) ≈ Ap (Extend ℓ f fs) (Extend ℓ τ r)))
-> Dict Unconstrained
-> Dict
     (Extend ℓ (f τ) (Ap fs r) ≈ Ap (Extend ℓ f fs) (Extend ℓ τ r))
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | Proof that the 'ApSingle' type family preserves labels and their ordering.
apSingleExtendSwap :: forall τ ℓ f r. Dict (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ)
apSingleExtendSwap :: Dict (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ)
apSingleExtendSwap = Dict Unconstrained
-> Dict (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ)
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict
      (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ))
-> Dict Unconstrained
-> Dict (Extend ℓ (f τ) (ApSingle r τ) ≈ ApSingle (Extend ℓ f r) τ)
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | Proof that the 'Ap' type family preserves labels and their ordering.
zipExtendSwap :: forall ℓ τ1 r1 τ2 r2. Dict (Extend ℓ (τ1, τ2) (Zip r1 r2) ≈ Zip (Extend ℓ τ1 r1) (Extend ℓ τ2 r2))
zipExtendSwap :: Dict
  (Extend ℓ (τ1, τ2) (Zip r1 r2)
   ≈ Zip (Extend ℓ τ1 r1) (Extend ℓ τ2 r2))
zipExtendSwap = Dict Unconstrained
-> Dict
     (Extend ℓ (τ1, τ2) (Zip r1 r2)
      ≈ Zip (Extend ℓ τ1 r1) (Extend ℓ τ2 r2))
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict
      (Extend ℓ (τ1, τ2) (Zip r1 r2)
       ≈ Zip (Extend ℓ τ1 r1) (Extend ℓ τ2 r2)))
-> Dict Unconstrained
-> Dict
     (Extend ℓ (τ1, τ2) (Zip r1 r2)
      ≈ Zip (Extend ℓ τ1 r1) (Extend ℓ τ2 r2))
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | Map preserves uniqueness of labels.
uniqueMap :: forall f r. Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
uniqueMap :: Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
uniqueMap = Dict Unconstrained
-> Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r))
-> Dict Unconstrained
-> Dict (AllUniqueLabels (Map f r) ≈ AllUniqueLabels r)
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | Ap preserves uniqueness of labels.
uniqueAp :: forall fs r. Dict (AllUniqueLabels (Ap fs r) ≈ AllUniqueLabels r)
uniqueAp :: Dict (AllUniqueLabels (Ap fs r) ≈ AllUniqueLabels r)
uniqueAp = Dict Unconstrained
-> Dict (AllUniqueLabels (Ap fs r) ≈ AllUniqueLabels r)
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict (AllUniqueLabels (Ap fs r) ≈ AllUniqueLabels r))
-> Dict Unconstrained
-> Dict (AllUniqueLabels (Ap fs r) ≈ AllUniqueLabels r)
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | ApSingle preserves uniqueness of labels.
uniqueApSingle :: forall x r. Dict (AllUniqueLabels (ApSingle r x) ≈ AllUniqueLabels r)
uniqueApSingle :: Dict (AllUniqueLabels (ApSingle r x) ≈ AllUniqueLabels r)
uniqueApSingle = Dict Unconstrained
-> Dict (AllUniqueLabels (ApSingle r x) ≈ AllUniqueLabels r)
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict (AllUniqueLabels (ApSingle r x) ≈ AllUniqueLabels r))
-> Dict Unconstrained
-> Dict (AllUniqueLabels (ApSingle r x) ≈ AllUniqueLabels r)
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | Zip preserves uniqueness of labels.
uniqueZip :: forall r1 r2. Dict (AllUniqueLabels (Zip r1 r2) ≈ (AllUniqueLabels r1, AllUniqueLabels r2))
uniqueZip :: Dict
  (AllUniqueLabels (Zip r1 r2)
   ≈ (AllUniqueLabels r1, AllUniqueLabels r2))
uniqueZip = Dict (Unconstrained, Unconstrained)
-> Dict
     (AllUniqueLabels (Zip r1 r2)
      ≈ (AllUniqueLabels r1, AllUniqueLabels r2))
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict (Unconstrained, Unconstrained)
 -> Dict
      (AllUniqueLabels (Zip r1 r2)
       ≈ (AllUniqueLabels r1, AllUniqueLabels r2)))
-> Dict (Unconstrained, Unconstrained)
-> Dict
     (AllUniqueLabels (Zip r1 r2)
      ≈ (AllUniqueLabels r1, AllUniqueLabels r2))
forall a b. (a -> b) -> a -> b
$ (Unconstrained, Unconstrained) =>
Dict (Unconstrained, Unconstrained)
forall (a :: Constraint). a => Dict a
Dict @(Unconstrained, Unconstrained)

-- | Map distributes over MinJoin
mapMinJoin :: forall f r r'. Dict (Map f r .\/ Map f r' ≈ Map f (r .\/ r'))
mapMinJoin :: Dict ((Map f r .\/ Map f r') ≈ Map f (r .\/ r'))
mapMinJoin = Dict Unconstrained
-> Dict ((Map f r .\/ Map f r') ≈ Map f (r .\/ r'))
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict ((Map f r .\/ Map f r') ≈ Map f (r .\/ r')))
-> Dict Unconstrained
-> Dict ((Map f r .\/ Map f r') ≈ Map f (r .\/ r'))
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | ApSingle distributes over MinJoin
apSingleMinJoin :: forall r r' x. Dict (ApSingle r x .\/ ApSingle r' x ≈ ApSingle (r .\/ r') x)
apSingleMinJoin :: Dict ((ApSingle r x .\/ ApSingle r' x) ≈ ApSingle (r .\/ r') x)
apSingleMinJoin = Dict Unconstrained
-> Dict ((ApSingle r x .\/ ApSingle r' x) ≈ ApSingle (r .\/ r') x)
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict ((ApSingle r x .\/ ApSingle r' x) ≈ ApSingle (r .\/ r') x))
-> Dict Unconstrained
-> Dict ((ApSingle r x .\/ ApSingle r' x) ≈ ApSingle (r .\/ r') x)
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | Two rows are subsets of a third if and only if their disjoint union is a
-- subset of that third.
subsetJoin :: forall r1 r2 s. Dict ((Subset r1 s, Subset r2 s) ≈ (Subset (r1 .+ r2) s))
subsetJoin :: Dict ((Subset r1 s, Subset r2 s) ≈ Subset (r1 .+ r2) s)
subsetJoin = Dict Unconstrained
-> Dict ((Subset r1 s, Subset r2 s) ≈ Subset (r1 .+ r2) s)
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict ((Subset r1 s, Subset r2 s) ≈ Subset (r1 .+ r2) s))
-> Dict Unconstrained
-> Dict ((Subset r1 s, Subset r2 s) ≈ Subset (r1 .+ r2) s)
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | If two rows are each subsets of a third, their join is a subset of the third
subsetJoin' :: forall r1 r2 s. Dict ((Subset r1 s, Subset r2 s) ≈ (Subset (r1 .// r2) s))
subsetJoin' :: Dict ((Subset r1 s, Subset r2 s) ≈ Subset (r1 .// r2) s)
subsetJoin' = Dict Unconstrained
-> Dict ((Subset r1 s, Subset r2 s) ≈ Subset (r1 .// r2) s)
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict ((Subset r1 s, Subset r2 s) ≈ Subset (r1 .// r2) s))
-> Dict Unconstrained
-> Dict ((Subset r1 s, Subset r2 s) ≈ Subset (r1 .// r2) s)
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | If a row is a subset of another, then its restriction is also a subset of the other
subsetRestrict :: forall r s l. (Subset r s) :- (Subset (r .- l) s)
subsetRestrict :: Subset r s :- Subset (r .- l) s
subsetRestrict = (Subset r s => Dict (Subset (r .- l) s))
-> Subset r s :- Subset (r .- l) s
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub ((Subset r s => Dict (Subset (r .- l) s))
 -> Subset r s :- Subset (r .- l) s)
-> (Subset r s => Dict (Subset (r .- l) s))
-> Subset r s :- Subset (r .- l) s
forall a b. (a -> b) -> a -> b
$ Dict Unconstrained -> Dict (Subset (r .- l) s)
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained -> Dict (Subset (r .- l) s))
-> Dict Unconstrained -> Dict (Subset (r .- l) s)
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | Subset is transitive
subsetTrans :: forall r1 r2 r3. (Subset r1 r2, Subset r2 r3) :- (Subset r1 r3)
subsetTrans :: (Subset r1 r2, Subset r2 r3) :- Subset r1 r3
subsetTrans = ((Subset r1 r2, Subset r2 r3) => Dict (Subset r1 r3))
-> (Subset r1 r2, Subset r2 r3) :- Subset r1 r3
forall (a :: Constraint) (b :: Constraint). (a => Dict b) -> a :- b
Sub (((Subset r1 r2, Subset r2 r3) => Dict (Subset r1 r3))
 -> (Subset r1 r2, Subset r2 r3) :- Subset r1 r3)
-> ((Subset r1 r2, Subset r2 r3) => Dict (Subset r1 r3))
-> (Subset r1 r2, Subset r2 r3) :- Subset r1 r3
forall a b. (a -> b) -> a -> b
$ Dict Unconstrained -> Dict (Subset r1 r3)
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained -> Dict (Subset r1 r3))
-> Dict Unconstrained -> Dict (Subset r1 r3)
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | Map distributes over Difference
mapDifference :: forall f r r'. Dict (Map f r .\\ Map f r' ≈ Map f (r .\\ r'))
mapDifference :: Dict ((Map f r .\\ Map f r') ≈ Map f (r .\\ r'))
mapDifference = Dict Unconstrained
-> Dict ((Map f r .\\ Map f r') ≈ Map f (r .\\ r'))
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict ((Map f r .\\ Map f r') ≈ Map f (r .\\ r')))
-> Dict Unconstrained
-> Dict ((Map f r .\\ Map f r') ≈ Map f (r .\\ r'))
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- | ApSingle distributes over Difference
apSingleDifference :: forall r r' x. Dict (ApSingle r x .\\ ApSingle r' x ≈ ApSingle (r .\\ r') x)
apSingleDifference :: Dict ((ApSingle r x .\\ ApSingle r' x) ≈ ApSingle (r .\\ r') x)
apSingleDifference = Dict Unconstrained
-> Dict ((ApSingle r x .\\ ApSingle r' x) ≈ ApSingle (r .\\ r') x)
forall a b. a -> b
UNSAFE.unsafeCoerce (Dict Unconstrained
 -> Dict ((ApSingle r x .\\ ApSingle r' x) ≈ ApSingle (r .\\ r') x))
-> Dict Unconstrained
-> Dict ((ApSingle r x .\\ ApSingle r' x) ≈ ApSingle (r .\\ r') x)
forall a b. (a -> b) -> a -> b
$ Unconstrained => Dict Unconstrained
forall (a :: Constraint). a => Dict a
Dict @Unconstrained

-- differenceForall :: forall r r' c. Forall r c :- Forall (r .\\ r') c