{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

-- The pattern completeness checker is much weaker before ghc-9.0. Rather than introducing redundant
-- cases and turning off the overlap check in newer ghc versions we disable the check for old
-- versions.
#if __GLASGOW_HASKELL__ < 900
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
#endif

module Constrained.Spec.Generics (
  GenericsFn,
  IsNormalType,
  fst_,
  snd_,
  pair_,
  left_,
  right_,
  cJust_,
  cNothing_,
  caseOn,
  branch,
  branchW,
  forAll',
  constrained',
  reify',
  con,
  onCon,
  isCon,
  sel,
  match,
  onJust,
  isJust,
  ifElse,
  chooseSpec,
) where

import Data.Typeable
import GHC.TypeLits (Symbol)
import GHC.TypeNats
import Test.QuickCheck (Arbitrary (..), oneof)

import Constrained.Base
import Constrained.Core
import Constrained.List
import Constrained.Spec.Pairs ()
import Constrained.Univ
import qualified Data.List.NonEmpty as NE

------------------------------------------------------------------------
-- Generics
------------------------------------------------------------------------

instance FunctionLike (GenericsFn fn) where
  sem :: forall (as :: [*]) b. GenericsFn fn as b -> FunTy as b
sem = \case
    GenericsFn fn as b
ToGeneric -> forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep
    GenericsFn fn as b
FromGeneric -> forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep

instance BaseUniverse fn => Functions (GenericsFn fn) fn where
  propagateSpecFun :: forall (as :: [*]) a b.
(TypeList as, Typeable as, HasSpec fn a, HasSpec fn b,
 All (HasSpec fn) as) =>
GenericsFn fn as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun GenericsFn fn as b
_ ListCtx Value as (HOLE a)
_ Specification fn b
TrueSpec = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
  propagateSpecFun GenericsFn fn as b
fn ListCtx Value as (HOLE a)
ctx (ExplainSpec [] Specification fn b
s) = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
 HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun GenericsFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
s
  propagateSpecFun GenericsFn fn as b
fn ListCtx Value as (HOLE a)
ctx (ExplainSpec [String]
es Specification fn b
s) = forall (fn :: [*] -> * -> *) a.
[String] -> Specification fn a -> Specification fn a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
 HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun GenericsFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
s
  propagateSpecFun GenericsFn fn as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
err) = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec NonEmpty String
err
  propagateSpecFun GenericsFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
spec = case GenericsFn fn as b
fn of
    GenericsFn fn as b
_
      | SuspendedSpec Var b
v Pred fn
ps <- Specification fn b
spec
      , ListCtx List Value as
pre HOLE a a
HOLE List Value as'
suf <- ListCtx Value as (HOLE a)
ctx ->
          forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
v' ->
            let args :: List (Term fn) (Append as (a : as'))
args = forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]).
List f as -> List f bs -> List f (Append as bs)
appendList (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as
pre) (Term fn a
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as'
suf)
             in forall (fn :: [*] -> * -> *) a. Term fn a -> Binder fn a -> Pred fn
Let (forall (as :: [*]) (fn :: [*] -> * -> *) a.
(Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn a,
 BaseUniverse fn) =>
fn as a -> List (Term fn) as -> Term fn a
App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn GenericsFn fn as b
fn) List (Term fn) (Append as (a : as'))
args) (Var b
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Pred fn -> Binder fn a
:-> Pred fn
ps)
    GenericsFn fn as b
ToGeneric | NilCtx HOLE a a
HOLE <- ListCtx Value as (HOLE a)
ctx -> case Specification fn b
spec of
      TypeSpec TypeSpec fn b
s OrdSet b
cant -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> OrdSet a -> Specification fn a
TypeSpec TypeSpec fn b
s (forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OrdSet b
cant)
      MemberSpec NonEmpty b
es -> forall a (fn :: [*] -> * -> *). NonEmpty a -> Specification fn a
MemberSpec (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HasSimpleRep a => SimpleRep a -> a
fromSimpleRep NonEmpty b
es)
    GenericsFn fn as b
FromGeneric | NilCtx HOLE a (SimpleRep b)
HOLE <- ListCtx Value as (HOLE a)
ctx -> case Specification fn b
spec of
      TypeSpec TypeSpec fn b
s OrdSet b
cant -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> OrdSet a -> Specification fn a
TypeSpec TypeSpec fn b
s (forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> OrdSet b
cant)
      MemberSpec NonEmpty b
es -> forall a (fn :: [*] -> * -> *). NonEmpty a -> Specification fn a
MemberSpec (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. HasSimpleRep a => a -> SimpleRep a
toSimpleRep NonEmpty b
es)

  rewriteRules :: forall (as :: [*]) b.
(TypeList as, Typeable as, HasSpec fn b, All (HasSpec fn) as) =>
GenericsFn fn as b -> List (Term fn) as -> Maybe (Term fn b)
rewriteRules GenericsFn fn as b
FromGeneric (App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fnU as b -> Maybe (fn as b)
extractFn @(GenericsFn fn) @fn -> Just GenericsFn fn as a
ToGeneric) (Term fn a
x :> List (Term fn) as1
Nil) :> List (Term fn) as1
_) = forall a b. (Typeable a, Typeable b) => a -> Maybe b
cast Term fn a
x
  rewriteRules GenericsFn fn as b
ToGeneric (App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fnU as b -> Maybe (fn as b)
extractFn @(GenericsFn fn) @fn -> Just GenericsFn fn as a
FromGeneric) (Term fn a
x :> List (Term fn) as1
Nil) :> List (Term fn) as1
_) = forall a. a -> Maybe a
Just Term fn a
x
  rewriteRules GenericsFn fn as b
_ List (Term fn) as
_ = forall a. Maybe a
Nothing

  mapTypeSpec :: forall a b.
(HasSpec fn a, HasSpec fn b) =>
GenericsFn fn '[a] b -> TypeSpec fn a -> Specification fn b
mapTypeSpec GenericsFn fn '[a] b
f TypeSpec fn a
ts = case GenericsFn fn '[a] b
f of
    GenericsFn fn '[a] b
ToGeneric -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec TypeSpec fn a
ts
    GenericsFn fn '[a] b
FromGeneric -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec TypeSpec fn a
ts

-- HasSpec for various generic types --------------------------------------

instance HasSimpleRep (a, b)
instance HasSimpleRep (a, b, c)
instance HasSimpleRep (a, b, c, d)
instance HasSimpleRep (a, b, c, d, e)
instance HasSimpleRep (a, b, c, d, e, g)
instance HasSimpleRep (a, b, c, d, e, g, h)
instance HasSimpleRep (Maybe a)
instance HasSimpleRep (Either a b)

instance
  ( HasSpec fn a
  , HasSpec fn b
  ) =>
  HasSpec fn (a, b)
instance
  ( HasSpec fn a
  , HasSpec fn b
  , HasSpec fn c
  ) =>
  HasSpec fn (a, b, c)
instance
  ( HasSpec fn a
  , HasSpec fn b
  , HasSpec fn c
  , HasSpec fn d
  ) =>
  HasSpec fn (a, b, c, d)
instance
  ( HasSpec fn a
  , HasSpec fn b
  , HasSpec fn c
  , HasSpec fn d
  , HasSpec fn e
  ) =>
  HasSpec fn (a, b, c, d, e)
instance
  ( HasSpec fn a
  , HasSpec fn b
  , HasSpec fn c
  , HasSpec fn d
  , HasSpec fn e
  , HasSpec fn g
  ) =>
  HasSpec fn (a, b, c, d, e, g)
instance
  ( HasSpec fn a
  , HasSpec fn b
  , HasSpec fn c
  , HasSpec fn d
  , HasSpec fn e
  , HasSpec fn g
  , HasSpec fn h
  ) =>
  HasSpec fn (a, b, c, d, e, g, h)
instance
  (IsNormalType a, HasSpec fn a) =>
  HasSpec fn (Maybe a)
instance
  ( HasSpec fn a
  , IsNormalType a
  , HasSpec fn b
  , IsNormalType b
  ) =>
  HasSpec fn (Either a b)

------------------------------------------------------------------------
-- Sums
------------------------------------------------------------------------

instance BaseUniverse fn => Functions (SumFn fn) fn where
  propagateSpecFun :: forall (as :: [*]) a b.
(TypeList as, Typeable as, HasSpec fn a, HasSpec fn b,
 All (HasSpec fn) as) =>
SumFn fn as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun SumFn fn as b
_ ListCtx Value as (HOLE a)
_ Specification fn b
TrueSpec = forall (fn :: [*] -> * -> *) a. Specification fn a
TrueSpec
  propagateSpecFun SumFn fn as b
fn ListCtx Value as (HOLE a)
ctx (ExplainSpec [] Specification fn b
s) = forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
 HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun SumFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
s
  propagateSpecFun SumFn fn as b
fn ListCtx Value as (HOLE a)
ctx (ExplainSpec [String]
es Specification fn b
s) = forall (fn :: [*] -> * -> *) a.
[String] -> Specification fn a -> Specification fn a
ExplainSpec [String]
es forall a b. (a -> b) -> a -> b
$ forall (f :: [*] -> * -> *) (fn :: [*] -> * -> *) (as :: [*]) a b.
(Functions f fn, TypeList as, Typeable as, HasSpec fn a,
 HasSpec fn b, All (HasSpec fn) as) =>
f as b
-> ListCtx Value as (HOLE a)
-> Specification fn b
-> Specification fn a
propagateSpecFun SumFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
s
  propagateSpecFun SumFn fn as b
_ ListCtx Value as (HOLE a)
_ (ErrorSpec NonEmpty String
err) = forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec NonEmpty String
err
  propagateSpecFun SumFn fn as b
fn ListCtx Value as (HOLE a)
ctx Specification fn b
spec = case SumFn fn as b
fn of
    SumFn fn as b
_
      | SuspendedSpec Var b
v Pred fn
ps <- Specification fn b
spec
      , ListCtx List Value as
pre HOLE a a
HOLE List Value as'
suf <- ListCtx Value as (HOLE a)
ctx ->
          forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
v' ->
            let args :: List (Term fn) (Append as (a : as'))
args = forall {a} (f :: a -> *) (as :: [a]) (bs :: [a]).
List f as -> List f bs -> List f (Append as bs)
appendList (forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as
pre) (Term fn a
v' forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *) (g :: k -> *) (as :: [k]).
(forall (a :: k). f a -> g a) -> List f as -> List g as
mapList (\(Value a
a) -> forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
Lit a
a) List Value as'
suf)
             in forall (fn :: [*] -> * -> *) a. Term fn a -> Binder fn a -> Pred fn
Let (forall (as :: [*]) (fn :: [*] -> * -> *) a.
(Typeable as, TypeList as, All (HasSpec fn) as, HasSpec fn a,
 BaseUniverse fn) =>
fn as a -> List (Term fn) as -> Term fn a
App (forall (fn :: [*] -> * -> *) (fnU :: [*] -> * -> *) (as :: [*]) b.
Member fn fnU =>
fn as b -> fnU as b
injectFn SumFn fn as b
fn) List (Term fn) (Append as (a : as'))
args) (Var b
v forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Var a -> Pred fn -> Binder fn a
:-> Pred fn
ps)
    SumFn fn as b
InjLeft | NilCtx HOLE a a
HOLE <- ListCtx Value as (HOLE a)
ctx -> case Specification fn b
spec of
      TypeSpec (SumSpec Maybe (Int, Int)
_ Specification fn a
sl Specification fn b
_) [b]
cant -> Specification fn a
sl forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a
notEqualSpec [a
a | SumLeft a
a <- [b]
cant]
      MemberSpec NonEmpty b
es ->
        forall a (fn :: [*] -> * -> *).
[a] -> NonEmpty String -> Specification fn a
memberSpecList
          [a
a | SumLeft a
a <- forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es]
          ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
              String
"propagateSpecFun (InjLeft HOLE) on (MemberSpec es) with no SumLeft in es: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es)
          )
    SumFn fn as b
InjRight | NilCtx HOLE a b
HOLE <- ListCtx Value as (HOLE a)
ctx -> case Specification fn b
spec of
      TypeSpec (SumSpec Maybe (Int, Int)
_ Specification fn a
_ Specification fn a
sr) [b]
cant -> Specification fn a
sr forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a
notEqualSpec [a
a | SumRight a
a <- [b]
cant]
      MemberSpec NonEmpty b
es ->
        forall a (fn :: [*] -> * -> *).
[a] -> NonEmpty String -> Specification fn a
memberSpecList
          [a
a | SumRight a
a <- forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es]
          ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
              String
"propagateSpecFun (InjRight HOLE) on (MemberSpec es) with no SumRight in es: "
                forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. NonEmpty a -> [a]
NE.toList NonEmpty b
es)
          )

  -- NOTE: this function over-approximates and returns a liberal spec.
  mapTypeSpec :: forall a b.
(HasSpec fn a, HasSpec fn b) =>
SumFn fn '[a] b -> TypeSpec fn a -> Specification fn b
mapTypeSpec SumFn fn '[a] b
f TypeSpec fn a
ts = case SumFn fn '[a] b
f of
    -- TODO possibly not the right counts??
    SumFn fn '[a] b
InjLeft -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a b.
Maybe (Int, Int)
-> Specification fn a -> Specification fn b -> SumSpec fn a b
SumSpec forall a. Maybe a
Nothing (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec TypeSpec fn a
ts) (forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"mapTypeSpec InjLeft"))
    SumFn fn '[a] b
InjRight -> forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a b.
Maybe (Int, Int)
-> Specification fn a -> Specification fn b -> SumSpec fn a b
SumSpec forall a. Maybe a
Nothing (forall (fn :: [*] -> * -> *) a.
NonEmpty String -> Specification fn a
ErrorSpec (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"mapTypeSpec InjRight")) (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
TypeSpec fn a -> Specification fn a
typeSpec TypeSpec fn a
ts)

------------------------------------------------------------------------
-- Syntax
------------------------------------------------------------------------

fst_ ::
  forall fn a b.
  ( HasSpec fn a
  , HasSpec fn b
  ) =>
  Term fn (a, b) ->
  Term fn a
fst_ :: forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn a
fst_ = forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @0

snd_ ::
  forall fn a b.
  ( HasSpec fn a
  , HasSpec fn b
  ) =>
  Term fn (a, b) ->
  Term fn b
snd_ :: forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn b
snd_ = forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel @1

pair_ ::
  forall fn a b.
  ( HasSpec fn a
  , HasSpec fn b
  ) =>
  Term fn a ->
  Term fn b ->
  Term fn (a, b)
pair_ :: forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Term fn (a, b)
pair_ Term fn a
a Term fn b
b = forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn (SimpleRep a) -> Term fn a
fromGeneric_ forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[a, b] (Prod a b)
pairFn Term fn a
a Term fn b
b

left_ ::
  ( HasSpec fn a
  , HasSpec fn b
  , IsNormalType a
  , IsNormalType b
  ) =>
  Term fn a ->
  Term fn (Either a b)
left_ :: forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) =>
Term fn a -> Term fn (Either a b)
left_ = forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn (SimpleRep a) -> Term fn a
fromGeneric_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) a b.
Member (SumFn fn) fn =>
fn '[a] (Sum a b)
injLeftFn

right_ ::
  ( HasSpec fn a
  , HasSpec fn b
  , IsNormalType a
  , IsNormalType b
  ) =>
  Term fn b ->
  Term fn (Either a b)
right_ :: forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b, IsNormalType a, IsNormalType b) =>
Term fn b -> Term fn (Either a b)
right_ = forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn (SimpleRep a) -> Term fn a
fromGeneric_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) a b.
Member (SumFn fn) fn =>
fn '[b] (Sum a b)
injRightFn

caseOn ::
  forall fn a.
  ( HasSpec fn a
  , HasSpec fn (SimpleRep a)
  , HasSimpleRep a
  , TypeSpec fn a ~ TypeSpec fn (SimpleRep a)
  , SimpleRep a ~ SumOver (Cases (SimpleRep a))
  , TypeList (Cases (SimpleRep a))
  ) =>
  Term fn a ->
  FunTy (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn :: forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn a
tm = forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(List f ts -> r) -> FunTy (MapList f ts) r
curryList @(Cases (SimpleRep a)) (forall (fn :: [*] -> * -> *) (as :: [*]).
HasSpec fn (SumOver as) =>
Term fn (SumOver as) -> List (Weighted (Binder fn)) as -> Pred fn
mkCase (forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn a -> Term fn (SimpleRep a)
toGeneric_ Term fn a
tm))

branch ::
  forall fn p a.
  ( HasSpec fn a
  , All (HasSpec fn) (Args a)
  , IsPred p fn
  , IsProd a
  ) =>
  FunTy (MapList (Term fn) (Args a)) p ->
  Weighted (Binder fn) a
branch :: forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch FunTy (MapList (Term fn) (Args a)) p
body =
  -- NOTE: It's not sufficient to simply apply `body` to all the arguments
  -- with `uncurryList` because that will mean that `var` is repeated in the
  -- body. For example, consider `branch $ \ i j -> i <=. j`. If we don't
  -- build the lets this will boil down to `p :-> fst p <=. snd p` which
  -- will blow up at generation time. If we instead do: `p :-> Let x (fst p) (Let y (snd p) (x <=. y))`
  -- the solver will solve `x` and `y` separately (`y` before `x` in this case) and things
  -- will work just fine.
  forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted forall a. Maybe a
Nothing (forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, IsPred p fn) =>
(Term fn a -> p) -> Binder fn a
bind (forall p (fn :: [*] -> * -> *) (as :: [*]).
(All (HasSpec fn) as, IsPred p fn, BaseUniverse fn) =>
FunTy (MapList (Term fn) as) p -> List (Term fn) as -> Pred fn
buildBranch @p @fn FunTy (MapList (Term fn) (Args a)) p
body forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p (fn :: [*] -> * -> *).
(IsProd p, HasSpec fn p, BaseUniverse fn) =>
Term fn p -> List (Term fn) (Args p)
toArgs @a @fn))

branchW ::
  forall fn p a.
  ( HasSpec fn a
  , All (HasSpec fn) (Args a)
  , IsPred p fn
  , IsProd a
  ) =>
  Int ->
  FunTy (MapList (Term fn) (Args a)) p ->
  Weighted (Binder fn) a
branchW :: forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
w FunTy (MapList (Term fn) (Args a)) p
body =
  forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted (forall a. a -> Maybe a
Just Int
w) (forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, IsPred p fn) =>
(Term fn a -> p) -> Binder fn a
bind (forall p (fn :: [*] -> * -> *) (as :: [*]).
(All (HasSpec fn) as, IsPred p fn, BaseUniverse fn) =>
FunTy (MapList (Term fn) as) p -> List (Term fn) as -> Pred fn
buildBranch @p @fn FunTy (MapList (Term fn) (Args a)) p
body forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p (fn :: [*] -> * -> *).
(IsProd p, HasSpec fn p, BaseUniverse fn) =>
Term fn p -> List (Term fn) (Args p)
toArgs @a @fn))

type IsProductType fn a =
  ( HasSimpleRep a
  , Cases (SimpleRep a) ~ '[SimpleRep a]
  , SimpleRep a ~ SumOver (Cases (SimpleRep a))
  , IsProd (SimpleRep a)
  , HasSpec fn (SimpleRep a)
  , TypeSpec fn a ~ TypeSpec fn (SimpleRep a)
  , All (HasSpec fn) (ProductAsList a)
  )

type ProductAsList a = Args (SimpleRep a)

match ::
  forall fn p a.
  ( HasSpec fn a
  , IsProductType fn a
  , IsPred p fn
  ) =>
  Term fn a ->
  FunTy (MapList (Term fn) (ProductAsList a)) p ->
  Pred fn
match :: forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn a
p FunTy (MapList (Term fn) (Args (SimpleRep a))) p
m = forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn Term fn a
p (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch @fn @p FunTy (MapList (Term fn) (Args (SimpleRep a))) p
m)

buildBranch ::
  forall p fn as.
  ( All (HasSpec fn) as
  , IsPred p fn
  , BaseUniverse fn
  ) =>
  FunTy (MapList (Term fn) as) p ->
  List (Term fn) as ->
  Pred fn
buildBranch :: forall p (fn :: [*] -> * -> *) (as :: [*]).
(All (HasSpec fn) as, IsPred p fn, BaseUniverse fn) =>
FunTy (MapList (Term fn) as) p -> List (Term fn) as -> Pred fn
buildBranch FunTy (MapList (Term fn) as) p
bd List (Term fn) as
Nil = forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, PredLike p, UnivConstr p fn) =>
p -> Pred fn
toPred FunTy (MapList (Term fn) as) p
bd
buildBranch FunTy (MapList (Term fn) as) p
bd (Term fn a
t :> List (Term fn) as1
args) =
  forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, IsPred p fn) =>
Term fn a -> (Term fn a -> p) -> Pred fn
letBind Term fn a
t forall a b. (a -> b) -> a -> b
$ \Term fn a
x -> forall p (fn :: [*] -> * -> *) (as :: [*]).
(All (HasSpec fn) as, IsPred p fn, BaseUniverse fn) =>
FunTy (MapList (Term fn) as) p -> List (Term fn) as -> Pred fn
buildBranch @p @fn (FunTy (MapList (Term fn) as) p
bd Term fn a
x) List (Term fn) as1
args

type family Args t where
  Args (Prod a b) = a : Args b
  Args a = '[a]

class IsProd p where
  toArgs ::
    ( HasSpec fn p
    , BaseUniverse fn
    ) =>
    Term fn p ->
    List (Term fn) (Args p)

instance {-# OVERLAPPABLE #-} Args a ~ '[a] => IsProd a where
  toArgs :: forall (fn :: [*] -> * -> *).
(HasSpec fn a, BaseUniverse fn) =>
Term fn a -> List (Term fn) (Args a)
toArgs = (forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil)

instance IsProd b => IsProd (Prod a b) where
  toArgs :: forall (fn :: [*] -> * -> *).
(HasSpec fn (Prod a b), BaseUniverse fn) =>
Term fn (Prod a b) -> List (Term fn) (Args (Prod a b))
toArgs (Term fn (Prod a b)
p :: Term fn (Prod a b))
    | Evidence (Prerequisites fn (Prod a b))
Evidence <- forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Evidence (Prerequisites fn a)
prerequisites @fn @(Prod a b) = (forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] a
fstFn Term fn (Prod a b)
p) forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall p (fn :: [*] -> * -> *).
(IsProd p, HasSpec fn p, BaseUniverse fn) =>
Term fn p -> List (Term fn) (Args p)
toArgs (forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] b
sndFn Term fn (Prod a b)
p)

type family ResultType t where
  ResultType (a -> b) = ResultType b
  ResultType a = a

-- NOTE: `ResultType r ~ Term fn a` is NOT a redundant constraint,
-- removing it causes type inference to break elsewhere
con ::
  forall c a r fn.
  ( SimpleRep a ~ SOP (TheSop a)
  , TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a))
  , TypeList (ConstrOf c (TheSop a))
  , HasSpec fn a
  , HasSimpleRep a
  , r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a)
  , ResultType r ~ Term fn a
  , SOPTerm c fn (TheSop a)
  , ConstrTerm fn (ConstrOf c (TheSop a))
  ) =>
  r
con :: forall (c :: Symbol) a r (fn :: [*] -> * -> *).
(SimpleRep a ~ SOP (TheSop a),
 TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a)),
 TypeList (ConstrOf c (TheSop a)), HasSpec fn a, HasSimpleRep a,
 r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a),
 ResultType r ~ Term fn a, SOPTerm c fn (TheSop a),
 ConstrTerm fn (ConstrOf c (TheSop a))) =>
r
con =
  forall (ts :: [*]) (f :: * -> *) r.
TypeList ts =>
(List f ts -> r) -> FunTy (MapList f ts) r
curryList @(ConstrOf c (TheSop a)) @(Term fn)
    (forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app (forall (fn :: [*] -> * -> *) a.
(HasSpec fn (SimpleRep a),
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) =>
fn '[SimpleRep a] a
fromGenericFn @_ @a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: Symbol) (fn :: [*] -> * -> *) (sop :: [*]).
SOPTerm c fn sop =>
Term fn (ProdOver (ConstrOf c sop)) -> Term fn (SOP sop)
inj_ @c @fn @(TheSop a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *) (constr :: [*]).
ConstrTerm fn constr =>
List (Term fn) constr -> Term fn (ProdOver constr)
prod_)

cJust_ :: (HasSpec fn a, IsNormalType a) => Term fn a -> Term fn (Maybe a)
cJust_ :: forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn a -> Term fn (Maybe a)
cJust_ = forall (c :: Symbol) a r (fn :: [*] -> * -> *).
(SimpleRep a ~ SOP (TheSop a),
 TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a)),
 TypeList (ConstrOf c (TheSop a)), HasSpec fn a, HasSimpleRep a,
 r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a),
 ResultType r ~ Term fn a, SOPTerm c fn (TheSop a),
 ConstrTerm fn (ConstrOf c (TheSop a))) =>
r
con @"Just"

cNothing_ :: (HasSpec fn a, IsNormalType a) => Term fn (Maybe a)
cNothing_ :: forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn (Maybe a)
cNothing_ = forall (c :: Symbol) a r (fn :: [*] -> * -> *).
(SimpleRep a ~ SOP (TheSop a),
 TypeSpec fn a ~ TypeSpec fn (SOP (TheSop a)),
 TypeList (ConstrOf c (TheSop a)), HasSpec fn a, HasSimpleRep a,
 r ~ FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) (Term fn a),
 ResultType r ~ Term fn a, SOPTerm c fn (TheSop a),
 ConstrTerm fn (ConstrOf c (TheSop a))) =>
r
con @"Nothing" (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit ())

sel ::
  forall n fn a c as.
  ( SimpleRep a ~ ProdOver as
  , TheSop a ~ '[c ::: as]
  , TypeSpec fn a ~ TypeSpec fn (ProdOver as)
  , Select fn n as
  , HasSpec fn a
  , HasSpec fn (ProdOver as)
  , HasSimpleRep a
  ) =>
  Term fn a ->
  Term fn (At n as)
sel :: forall (n :: Natural) (fn :: [*] -> * -> *) a (c :: Symbol)
       (as :: [*]).
(SimpleRep a ~ ProdOver as, TheSop a ~ '[c ::: as],
 TypeSpec fn a ~ TypeSpec fn (ProdOver as), Select fn n as,
 HasSpec fn a, HasSpec fn (ProdOver as), HasSimpleRep a) =>
Term fn a -> Term fn (At n as)
sel = forall (fn :: [*] -> * -> *) (n :: Natural) (as :: [*]).
Select fn n as =>
Term fn (ProdOver as) -> Term fn (At n as)
select_ @fn @n @as forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn a -> Term fn (SimpleRep a)
toGeneric_

type family Cases t where
  Cases (Sum a b) = a : Cases b
  Cases a = '[a]

-- | Like `forAll` but pattern matches on the `Term fn a`
forAll' ::
  forall fn t a p.
  ( Forallable t a
  , Cases (SimpleRep a) ~ '[SimpleRep a]
  , TypeSpec fn a ~ TypeSpec fn (SimpleRep a)
  , HasSpec fn t
  , HasSpec fn (SimpleRep a)
  , HasSimpleRep a
  , All (HasSpec fn) (Args (SimpleRep a))
  , IsPred p fn
  , IsProd (SimpleRep a)
  , HasSpec fn a
  ) =>
  Term fn t ->
  FunTy (MapList (Term fn) (Args (SimpleRep a))) p ->
  Pred fn
forAll' :: forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term fn t
xs FunTy (MapList (Term fn) (Args (SimpleRep a))) p
f = forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn t
xs forall a b. (a -> b) -> a -> b
$ \Term fn a
x -> forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match @fn @p Term fn a
x FunTy (MapList (Term fn) (Args (SimpleRep a))) p
f

-- | Like `constrained` but pattern matches on the bound `Term fn a`
constrained' ::
  forall a fn p.
  ( Cases (SimpleRep a) ~ '[SimpleRep a]
  , TypeSpec fn a ~ TypeSpec fn (SimpleRep a)
  , HasSpec fn (SimpleRep a)
  , HasSimpleRep a
  , All (HasSpec fn) (Args (SimpleRep a))
  , IsProd (SimpleRep a)
  , HasSpec fn a
  , IsPred p fn
  ) =>
  FunTy (MapList (Term fn) (Args (SimpleRep a))) p ->
  Specification fn a
constrained' :: forall a (fn :: [*] -> * -> *) p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsProd (SimpleRep a),
 HasSpec fn a, IsPred p fn) =>
FunTy (MapList (Term fn) (Args (SimpleRep a))) p
-> Specification fn a
constrained' FunTy (MapList (Term fn) (Args (SimpleRep a))) p
f = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
x -> forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match @fn @p Term fn a
x FunTy (MapList (Term fn) (Args (SimpleRep a))) p
f

-- | Like `reify` but pattern matches on the bound `Term fn b`
reify' ::
  forall fn a b p.
  ( Cases (SimpleRep b) ~ '[SimpleRep b]
  , TypeSpec fn b ~ TypeSpec fn (SimpleRep b)
  , HasSpec fn (SimpleRep b)
  , HasSimpleRep b
  , All (HasSpec fn) (Args (SimpleRep b))
  , IsProd (SimpleRep b)
  , HasSpec fn a
  , HasSpec fn b
  , IsPred p fn
  ) =>
  Term fn a ->
  (a -> b) ->
  FunTy (MapList (Term fn) (Args (SimpleRep b))) p ->
  Pred fn
reify' :: forall (fn :: [*] -> * -> *) a b p.
(Cases (SimpleRep b) ~ '[SimpleRep b],
 TypeSpec fn b ~ TypeSpec fn (SimpleRep b),
 HasSpec fn (SimpleRep b), HasSimpleRep b,
 All (HasSpec fn) (Args (SimpleRep b)), IsProd (SimpleRep b),
 HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a
-> (a -> b)
-> FunTy (MapList (Term fn) (Args (SimpleRep b))) p
-> Pred fn
reify' Term fn a
a a -> b
r FunTy (MapList (Term fn) (Args (SimpleRep b))) p
f = forall (fn :: [*] -> * -> *) a b p.
(HasSpec fn a, HasSpec fn b, IsPred p fn) =>
Term fn a -> (a -> b) -> (Term fn b -> p) -> Pred fn
reify Term fn a
a a -> b
r forall a b. (a -> b) -> a -> b
$ \Term fn b
x -> forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match @fn @p Term fn b
x FunTy (MapList (Term fn) (Args (SimpleRep b))) p
f

class (BaseUniverse fn, HasSpec fn (SOP sop)) => SOPTerm c fn sop where
  inj_ :: Term fn (ProdOver (ConstrOf c sop)) -> Term fn (SOP sop)

instance HasSpec fn (ProdOver constr) => SOPTerm c fn (c ::: constr : '[]) where
  inj_ :: Term fn (ProdOver (ConstrOf c '[c ::: constr]))
-> Term fn (SOP '[c ::: constr])
inj_ = forall a. a -> a
id

instance
  ( HasSpec fn (SOP (con : sop))
  , HasSpec fn (ProdOver constr)
  , KnownNat (CountCases (SOP (con : sop)))
  ) =>
  SOPTerm c fn (c ::: constr : con : sop)
  where
  inj_ :: Term fn (ProdOver (ConstrOf c ((c ::: constr) : con : sop)))
-> Term fn (SOP ((c ::: constr) : con : sop))
inj_ = forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) a b.
Member (SumFn fn) fn =>
fn '[a] (Sum a b)
injLeftFn

instance
  {-# OVERLAPPABLE #-}
  ( HasSpec fn (ProdOver con)
  , SOPTerm c fn (con' : sop)
  , ConstrOf c (con' : sop) ~ ConstrOf c ((c' ::: con) : con' : sop)
  , KnownNat (CountCases (SOP (con' : sop)))
  ) =>
  SOPTerm c fn ((c' ::: con) : con' : sop)
  where
  inj_ :: Term fn (ProdOver (ConstrOf c ((c' ::: con) : con' : sop)))
-> Term fn (SOP ((c' ::: con) : con' : sop))
inj_ = forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) a b.
Member (SumFn fn) fn =>
fn '[b] (Sum a b)
injRightFn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: Symbol) (fn :: [*] -> * -> *) (sop :: [*]).
SOPTerm c fn sop =>
Term fn (ProdOver (ConstrOf c sop)) -> Term fn (SOP sop)
inj_ @c @fn @(con' : sop)

class (BaseUniverse fn, HasSpec fn (ProdOver constr)) => ConstrTerm fn constr where
  prod_ :: List (Term fn) constr -> Term fn (ProdOver constr)

instance HasSpec fn a => ConstrTerm fn '[a] where
  prod_ :: List (Term fn) '[a] -> Term fn (ProdOver '[a])
prod_ (Term fn a
a :> List (Term fn) as1
Nil) = Term fn a
a

instance
  ( HasSpec fn a
  , HasSpec fn (ProdOver (a : b : as))
  , ConstrTerm fn (b : as)
  ) =>
  ConstrTerm fn (a : b : as)
  where
  prod_ :: List (Term fn) (a : b : as) -> Term fn (ProdOver (a : b : as))
prod_ (Term fn a
a :> List (Term fn) as1
as) = forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[a, b] (Prod a b)
pairFn Term fn a
a (forall (fn :: [*] -> * -> *) (constr :: [*]).
ConstrTerm fn constr =>
List (Term fn) constr -> Term fn (ProdOver constr)
prod_ List (Term fn) as1
as)

type family At n as where
  At 0 (a : as) = a
  At n (a : as) = At (n - 1) as

class Select fn n as where
  select_ :: Term fn (ProdOver as) -> Term fn (At n as)

instance Select fn 0 (a : '[]) where
  select_ :: Term fn (ProdOver '[a]) -> Term fn (At 0 '[a])
select_ = forall a. a -> a
id

instance (HasSpec fn a, HasSpec fn (ProdOver (a' : as))) => Select fn 0 (a : a' : as) where
  select_ :: Term fn (ProdOver (a : a' : as)) -> Term fn (At 0 (a : a' : as))
select_ = forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] a
fstFn

instance
  {-# OVERLAPPABLE #-}
  ( HasSpec fn a
  , HasSpec fn (ProdOver (a' : as))
  , At (n - 1) (a' : as) ~ At n (a : a' : as)
  , Select fn (n - 1) (a' : as)
  ) =>
  Select fn n (a : a' : as)
  where
  select_ :: Term fn (ProdOver (a : a' : as)) -> Term fn (At n (a : a' : as))
select_ = forall (fn :: [*] -> * -> *) (n :: Natural) (as :: [*]).
Select fn n as =>
Term fn (ProdOver as) -> Term fn (At n as)
select_ @fn @(n - 1) @(a' : as) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *) b (as :: [*]).
(HasSpec fn b, Typeable as, TypeList as, All (HasSpec fn) as) =>
fn as b -> FunTy (MapList (Term fn) as) (Term fn b)
app forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] b
sndFn

class IsConstrOf (c :: Symbol) b sop where
  mkCases ::
    (HasSpec fn b, All (HasSpec fn) (Cases (SOP sop))) =>
    (forall a. Term fn a -> Pred fn) ->
    (Term fn b -> Pred fn) ->
    List (Weighted (Binder fn)) (Cases (SOP sop))

instance
  ( b ~ ProdOver as
  , TypeList (Cases (SOP (con : sop)))
  ) =>
  IsConstrOf c b ((c ::: as) : con : sop)
  where
  mkCases :: forall (fn :: [*] -> * -> *).
(HasSpec fn b,
 All (HasSpec fn) (Cases (SOP ((c ::: as) : con : sop)))) =>
(forall a. Term fn a -> Pred fn)
-> (Term fn b -> Pred fn)
-> List
     (Weighted (Binder fn)) (Cases (SOP ((c ::: as) : con : sop)))
mkCases forall a. Term fn a -> Pred fn
r (Term fn b -> Pred fn
k :: Term fn b -> Pred fn) =
    forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted forall a. Maybe a
Nothing (forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, IsPred p fn) =>
(Term fn a -> p) -> Binder fn a
bind Term fn b -> Pred fn
k)
      forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (c :: k -> Constraint) (as :: [k]) (f :: k -> *)
       (g :: k -> *).
All c as =>
(forall (a :: k). c a => f a -> g a) -> List f as -> List g as
mapListC @(HasSpec fn) (\Const () a
_ -> forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted forall a. Maybe a
Nothing (forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, IsPred p fn) =>
(Term fn a -> p) -> Binder fn a
bind forall a. Term fn a -> Pred fn
r)) (forall (as :: [*]). TypeList as => List (Const ()) as
listShape @(Cases (SOP (con : sop))))

instance
  ( b ~ ProdOver as
  , IsNormalType b
  ) =>
  IsConstrOf c b '[c ::: as]
  where
  mkCases :: forall (fn :: [*] -> * -> *).
(HasSpec fn b, All (HasSpec fn) (Cases (SOP '[c ::: as]))) =>
(forall a. Term fn a -> Pred fn)
-> (Term fn b -> Pred fn)
-> List (Weighted (Binder fn)) (Cases (SOP '[c ::: as]))
mkCases forall a. Term fn a -> Pred fn
_ (Term fn b -> Pred fn
k :: Term fn b -> Pred fn) = forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted forall a. Maybe a
Nothing (forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, IsPred p fn) =>
(Term fn a -> p) -> Binder fn a
bind Term fn b -> Pred fn
k) forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall {k} (f :: k -> *). List f '[]
Nil

instance
  {-# OVERLAPPABLE #-}
  ( Cases (SOP ((c' ::: as) : cs)) ~ (ProdOver as : Cases (SOP cs))
  , IsConstrOf c b cs
  ) =>
  IsConstrOf c b ((c' ::: as) : cs)
  where
  mkCases :: forall (fn :: [*] -> * -> *).
(HasSpec fn b,
 All (HasSpec fn) (Cases (SOP ((c' ::: as) : cs)))) =>
(forall a. Term fn a -> Pred fn)
-> (Term fn b -> Pred fn)
-> List (Weighted (Binder fn)) (Cases (SOP ((c' ::: as) : cs)))
mkCases forall a. Term fn a -> Pred fn
r Term fn b -> Pred fn
k = forall (f :: * -> *) a. Maybe Int -> f a -> Weighted f a
Weighted forall a. Maybe a
Nothing (forall (fn :: [*] -> * -> *) a p.
(HasSpec fn a, IsPred p fn) =>
(Term fn a -> p) -> Binder fn a
bind (forall a. Term fn a -> Pred fn
r @(ProdOver as))) forall {k} (f :: k -> *) (a :: k) (as1 :: [k]).
f a -> List f as1 -> List f (a : as1)
:> forall (c :: Symbol) b (sop :: [*]) (fn :: [*] -> * -> *).
(IsConstrOf c b sop, HasSpec fn b,
 All (HasSpec fn) (Cases (SOP sop))) =>
(forall a. Term fn a -> Pred fn)
-> (Term fn b -> Pred fn)
-> List (Weighted (Binder fn)) (Cases (SOP sop))
mkCases @c @_ @cs forall a. Term fn a -> Pred fn
r Term fn b -> Pred fn
k

-- TODO: the constraints around this are horrible!! We should figure out a way to make these things nicer.
onCon ::
  forall c a fn p.
  ( IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a)
  , TypeSpec fn a ~ TypeSpec fn (SimpleRep a)
  , HasSimpleRep a
  , HasSpec fn a
  , HasSpec fn (SimpleRep a)
  , SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a
  , All (HasSpec fn) (Cases (SOP (TheSop a)))
  , HasSpec fn (ProdOver (ConstrOf c (TheSop a)))
  , IsPred p fn
  , Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a)
  , All (HasSpec fn) (ConstrOf c (TheSop a))
  , IsProd (ProdOver (ConstrOf c (TheSop a)))
  ) =>
  Term fn a ->
  FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p ->
  Pred fn
onCon :: forall (c :: Symbol) a (fn :: [*] -> * -> *) p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a,
 HasSpec fn a, HasSpec fn (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All (HasSpec fn) (Cases (SOP (TheSop a))),
 HasSpec fn (ProdOver (ConstrOf c (TheSop a))), IsPred p fn,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All (HasSpec fn) (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term fn a
-> FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p -> Pred fn
onCon Term fn a
tm FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p
p =
  forall (fn :: [*] -> * -> *) (as :: [*]).
HasSpec fn (SumOver as) =>
Term fn (SumOver as) -> List (Weighted (Binder fn)) as -> Pred fn
Case
    (forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn a -> Term fn (SimpleRep a)
toGeneric_ Term fn a
tm)
    ( forall (c :: Symbol) b (sop :: [*]) (fn :: [*] -> * -> *).
(IsConstrOf c b sop, HasSpec fn b,
 All (HasSpec fn) (Cases (SOP sop))) =>
(forall a. Term fn a -> Pred fn)
-> (Term fn b -> Pred fn)
-> List (Weighted (Binder fn)) (Cases (SOP sop))
mkCases @c @(ProdOver (ConstrOf c (TheSop a))) @(TheSop a)
        (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert Bool
True)
        (forall p (fn :: [*] -> * -> *) (as :: [*]).
(All (HasSpec fn) as, IsPred p fn, BaseUniverse fn) =>
FunTy (MapList (Term fn) as) p -> List (Term fn) as -> Pred fn
buildBranch @p FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall p (fn :: [*] -> * -> *).
(IsProd p, HasSpec fn p, BaseUniverse fn) =>
Term fn p -> List (Term fn) (Args p)
toArgs)
    )

isCon ::
  forall c a fn.
  ( IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a)
  , TypeSpec fn a ~ TypeSpec fn (SimpleRep a)
  , HasSimpleRep a
  , HasSpec fn a
  , HasSpec fn (SimpleRep a)
  , SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a
  , All (HasSpec fn) (Cases (SOP (TheSop a)))
  , HasSpec fn (ProdOver (ConstrOf c (TheSop a)))
  ) =>
  Term fn a ->
  Pred fn
isCon :: forall (c :: Symbol) a (fn :: [*] -> * -> *).
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a,
 HasSpec fn a, HasSpec fn (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All (HasSpec fn) (Cases (SOP (TheSop a))),
 HasSpec fn (ProdOver (ConstrOf c (TheSop a)))) =>
Term fn a -> Pred fn
isCon Term fn a
tm =
  forall (fn :: [*] -> * -> *) (as :: [*]).
HasSpec fn (SumOver as) =>
Term fn (SumOver as) -> List (Weighted (Binder fn)) as -> Pred fn
Case
    (forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn a -> Term fn (SimpleRep a)
toGeneric_ Term fn a
tm)
    ( forall (c :: Symbol) b (sop :: [*]) (fn :: [*] -> * -> *).
(IsConstrOf c b sop, HasSpec fn b,
 All (HasSpec fn) (Cases (SOP sop))) =>
(forall a. Term fn a -> Pred fn)
-> (Term fn b -> Pred fn)
-> List (Weighted (Binder fn)) (Cases (SOP sop))
mkCases @c @(ProdOver (ConstrOf c (TheSop a))) @(TheSop a)
        (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert Bool
False)
        (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert Bool
True)
    )

type IsNormalType a = (Cases a ~ '[a], Args a ~ '[a], IsProd a, CountCases a ~ 1)

onJust ::
  forall fn a p.
  (BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
  Term fn (Maybe a) ->
  (Term fn a -> p) ->
  Pred fn
onJust :: forall (fn :: [*] -> * -> *) a p.
(BaseUniverse fn, HasSpec fn a, IsNormalType a, IsPred p fn) =>
Term fn (Maybe a) -> (Term fn a -> p) -> Pred fn
onJust = forall (c :: Symbol) a (fn :: [*] -> * -> *) p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a,
 HasSpec fn a, HasSpec fn (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All (HasSpec fn) (Cases (SOP (TheSop a))),
 HasSpec fn (ProdOver (ConstrOf c (TheSop a))), IsPred p fn,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All (HasSpec fn) (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term fn a
-> FunTy (MapList (Term fn) (ConstrOf c (TheSop a))) p -> Pred fn
onCon @"Just"

isJust ::
  forall fn a.
  (BaseUniverse fn, HasSpec fn a, IsNormalType a) =>
  Term fn (Maybe a) ->
  Pred fn
isJust :: forall (fn :: [*] -> * -> *) a.
(BaseUniverse fn, HasSpec fn a, IsNormalType a) =>
Term fn (Maybe a) -> Pred fn
isJust = forall (c :: Symbol) a (fn :: [*] -> * -> *).
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a,
 HasSpec fn a, HasSpec fn (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All (HasSpec fn) (Cases (SOP (TheSop a))),
 HasSpec fn (ProdOver (ConstrOf c (TheSop a)))) =>
Term fn a -> Pred fn
isCon @"Just"

chooseSpec ::
  HasSpec fn a =>
  (Int, Specification fn a) ->
  (Int, Specification fn a) ->
  Specification fn a
chooseSpec :: forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
(Int, Specification fn a)
-> (Int, Specification fn a) -> Specification fn a
chooseSpec (Int
w, Specification fn a
s) (Int
w', Specification fn a
s') =
  forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn a
x ->
    forall a p (fn :: [*] -> * -> *).
(HasSpec fn a, IsPred p fn) =>
((forall b. Term fn b -> b) -> GE a) -> (Term fn a -> p) -> Pred fn
exists (\forall b. Term fn b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall b. Term fn b -> b
eval Term fn a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
a -> Specification fn a -> Bool
`conformsToSpec` Specification fn a
s) forall a b. (a -> b) -> a -> b
$ \Term fn Bool
b ->
      [ forall (fn :: [*] -> * -> *) p q.
(BaseUniverse fn, IsPred p fn, IsPred q fn) =>
Term fn Bool -> p -> q -> Pred fn
ifElse
          Term fn Bool
b
          (Term fn a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
s)
          (Term fn a
x forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
`satisfies` Specification fn a
s')
      , forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
          Term fn Bool
b
          (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
w' forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Bool
True)
          (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
Int
-> FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branchW Int
w forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Bool
True)
      ]

-- Arbitrary instances ----------------------------------------------------

instance
  (HasSpec fn a, HasSpec fn b, Arbitrary (FoldSpec fn a), Arbitrary (FoldSpec fn b)) =>
  Arbitrary (FoldSpec fn (a, b))
  where
  arbitrary :: Gen (FoldSpec fn (a, b))
arbitrary =
    forall a. HasCallStack => [Gen a] -> Gen a
oneof
      [ forall (fn :: [*] -> * -> *) a b.
HasSpec fn a =>
fn '[a] b -> FoldSpec fn b -> FoldSpec fn a
preMapFoldSpec (forall (fn :: [*] -> * -> *) b a c.
(Member (FunFn fn) fn, HasSpec fn b, Show (fn '[a] b),
 Show (fn '[b] c), Eq (fn '[a] b), Eq (fn '[b] c)) =>
fn '[b] c -> fn '[a] b -> fn '[a] c
composeFn forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] a
fstFn forall (fn :: [*] -> * -> *) a.
(HasSpec fn (SimpleRep a),
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) =>
fn '[a] (SimpleRep a)
toGenericFn) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
      , forall (fn :: [*] -> * -> *) a b.
HasSpec fn a =>
fn '[a] b -> FoldSpec fn b -> FoldSpec fn a
preMapFoldSpec (forall (fn :: [*] -> * -> *) b a c.
(Member (FunFn fn) fn, HasSpec fn b, Show (fn '[a] b),
 Show (fn '[b] c), Eq (fn '[a] b), Eq (fn '[b] c)) =>
fn '[b] c -> fn '[a] b -> fn '[a] c
composeFn forall (fn :: [*] -> * -> *) a b.
Member (PairFn fn) fn =>
fn '[Prod a b] b
sndFn forall (fn :: [*] -> * -> *) a.
(HasSpec fn (SimpleRep a),
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSimpleRep a) =>
fn '[a] (SimpleRep a)
toGenericFn) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary
      , forall (f :: * -> *) a. Applicative f => a -> f a
pure forall (fn :: [*] -> * -> *) a. FoldSpec fn a
NoFold
      ]
  shrink :: FoldSpec fn (a, b) -> [FoldSpec fn (a, b)]
shrink FoldSpec fn (a, b)
NoFold = []
  shrink FoldSpec {} = [forall (fn :: [*] -> * -> *) a. FoldSpec fn a
NoFold]