module Rerefined.Refined1 where

import Language.Haskell.TH.Syntax ( Lift )

-- | @f a@ refined with predicate @p@.
newtype Refined1 p f a = Refined1 (f a)
    deriving stock ((forall (m :: Type -> Type). Quote m => Refined1 p f a -> m Exp)
-> (forall (m :: Type -> Type).
    Quote m =>
    Refined1 p f a -> Code m (Refined1 p f a))
-> Lift (Refined1 p f a)
forall k (p :: k) k (f :: k -> Type) (a :: k) (m :: Type -> Type).
(Lift (f a), Quote m) =>
Refined1 p f a -> m Exp
forall k (p :: k) k (f :: k -> Type) (a :: k) (m :: Type -> Type).
(Lift (f a), Quote m) =>
Refined1 p f a -> Code m (Refined1 p f a)
forall t.
(forall (m :: Type -> Type). Quote m => t -> m Exp)
-> (forall (m :: Type -> Type). Quote m => t -> Code m t) -> Lift t
forall (m :: Type -> Type). Quote m => Refined1 p f a -> m Exp
forall (m :: Type -> Type).
Quote m =>
Refined1 p f a -> Code m (Refined1 p f a)
$clift :: forall k (p :: k) k (f :: k -> Type) (a :: k) (m :: Type -> Type).
(Lift (f a), Quote m) =>
Refined1 p f a -> m Exp
lift :: forall (m :: Type -> Type). Quote m => Refined1 p f a -> m Exp
$cliftTyped :: forall k (p :: k) k (f :: k -> Type) (a :: k) (m :: Type -> Type).
(Lift (f a), Quote m) =>
Refined1 p f a -> Code m (Refined1 p f a)
liftTyped :: forall (m :: Type -> Type).
Quote m =>
Refined1 p f a -> Code m (Refined1 p f a)
Lift, Int -> Refined1 p f a -> ShowS
[Refined1 p f a] -> ShowS
Refined1 p f a -> String
(Int -> Refined1 p f a -> ShowS)
-> (Refined1 p f a -> String)
-> ([Refined1 p f a] -> ShowS)
-> Show (Refined1 p f a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (p :: k) k (f :: k -> Type) (a :: k).
Show (f a) =>
Int -> Refined1 p f a -> ShowS
forall k (p :: k) k (f :: k -> Type) (a :: k).
Show (f a) =>
[Refined1 p f a] -> ShowS
forall k (p :: k) k (f :: k -> Type) (a :: k).
Show (f a) =>
Refined1 p f a -> String
$cshowsPrec :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Show (f a) =>
Int -> Refined1 p f a -> ShowS
showsPrec :: Int -> Refined1 p f a -> ShowS
$cshow :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Show (f a) =>
Refined1 p f a -> String
show :: Refined1 p f a -> String
$cshowList :: forall k (p :: k) k (f :: k -> Type) (a :: k).
Show (f a) =>
[Refined1 p f a] -> ShowS
showList :: [Refined1 p f a] -> ShowS
Show) -- TODO Show? useful but meh?

-- | Strip the refinement from a 'Refined1'.
--
-- This is kept as a separate function for prettier @'Show' 'Refined1'@ output.
unrefine1 :: Refined1 p f a -> f a
unrefine1 :: forall {k} {k} (p :: k) (f :: k -> Type) (a :: k).
Refined1 p f a -> f a
unrefine1 (Refined1 f a
fa) = f a
fa