-- editorconfig-checker-disable-file
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE ViewPatterns          #-}

{-# OPTIONS_GHC -Wno-partial-type-signatures #-}

module PlutusIR.Generators.QuickCheck.ShrinkTerms where

import PlutusPrelude

import PlutusIR.Generators.QuickCheck.Common

import PlutusCore.Generators.QuickCheck.Common
import PlutusCore.Generators.QuickCheck.ShrinkTypes
import PlutusCore.Generators.QuickCheck.Substitutions
import PlutusCore.Generators.QuickCheck.Utils

import PlutusCore.Builtin
import PlutusCore.Crypto.BLS12_381.G1 qualified as BLS12_381.G1 (offchain_zero)
import PlutusCore.Crypto.BLS12_381.G2 qualified as BLS12_381.G2 (offchain_zero)
import PlutusCore.Crypto.BLS12_381.Pairing qualified as BLS12_381.Pairing (identityMlResult)
import PlutusCore.Data
import PlutusCore.Default
import PlutusCore.MkPlc (mkConstantOf, mkTyBuiltinOf)
import PlutusCore.Name.Unique
import PlutusCore.Pretty
import PlutusCore.Subst (typeSubstClosedType)
import PlutusIR
import PlutusIR.Subst

import Data.Bifunctor
import Data.Map.Strict (Map)
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Data.Set.Lens (setOf)
import GHC.Stack
import Test.QuickCheck (shrink, shrinkList)

addTmBind :: Binding TyName Name DefaultUni DefaultFun ()
          -> Map Name (Type TyName DefaultUni ())
          -> Map Name (Type TyName DefaultUni ())
addTmBind :: Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind (TermBind ()
_ Strictness
_ (VarDecl ()
_ Name
x Type TyName DefaultUni ()
a) Term TyName Name DefaultUni DefaultFun ()
_) = Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a
addTmBind (DatatypeBind ()
_ Datatype TyName Name DefaultUni ()
dat)             = ([(Name, Type TyName DefaultUni ())]
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (Datatype TyName Name DefaultUni ()
-> (Name, Type TyName DefaultUni ())
matchType Datatype TyName Name DefaultUni ()
dat (Name, Type TyName DefaultUni ())
-> [(Name, Type TyName DefaultUni ())]
-> [(Name, Type TyName DefaultUni ())]
forall a. a -> [a] -> [a]
: Datatype TyName Name DefaultUni ()
-> [(Name, Type TyName DefaultUni ())]
constrTypes Datatype TyName Name DefaultUni ()
dat) Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall a. Semigroup a => a -> a -> a
<>)
addTmBind Binding TyName Name DefaultUni DefaultFun ()
_                                = Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall a. a -> a
id

scopeCheckTyVars :: TypeCtx
                 -> (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
                 -> Bool
scopeCheckTyVars :: TypeCtx
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> Bool
scopeCheckTyVars TypeCtx
tyctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm) = Getting (Set TyName) (Type TyName DefaultUni ()) TyName
-> Type TyName DefaultUni () -> Set TyName
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set TyName) (Type TyName DefaultUni ()) TyName
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
Traversal' (Type tyname uni ann) tyname
Traversal' (Type TyName DefaultUni ()) TyName
ftvTy Type TyName DefaultUni ()
ty Set TyName -> Set TyName -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set TyName
inscope
  where
    inscope :: Set TyName
inscope = TypeCtx -> Set TyName
forall k a. Map k a -> Set k
Map.keysSet TypeCtx
tyctx Set TyName -> Set TyName -> Set TyName
forall a. Semigroup a => a -> a -> a
<> [TyName] -> Set TyName
forall a. Ord a => [a] -> Set a
Set.fromList (((TyName, Kind ()) -> TyName) -> [(TyName, Kind ())] -> [TyName]
forall a b. (a -> b) -> [a] -> [b]
map (TyName, Kind ()) -> TyName
forall a b. (a, b) -> a
fst ([(TyName, Kind ())] -> [TyName])
-> [(TyName, Kind ())] -> [TyName]
forall a b. (a -> b) -> a -> b
$ Term TyName Name DefaultUni DefaultFun () -> [(TyName, Kind ())]
datatypes Term TyName Name DefaultUni DefaultFun ()
tm)

-- | Try to find a variable of type `forall x. x` in the context.
findHelp :: Map Name (Type TyName DefaultUni ()) -> Maybe Name
findHelp :: Map Name (Type TyName DefaultUni ()) -> Maybe Name
findHelp Map Name (Type TyName DefaultUni ())
ctx =
  case Map Name (Type TyName DefaultUni ())
-> [(Name, Type TyName DefaultUni ())]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Name (Type TyName DefaultUni ())
 -> [(Name, Type TyName DefaultUni ())])
-> Map Name (Type TyName DefaultUni ())
-> [(Name, Type TyName DefaultUni ())]
forall a b. (a -> b) -> a -> b
$ (Type TyName DefaultUni () -> Bool)
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter Type TyName DefaultUni () -> Bool
forall {a} {uni :: * -> *}. Eq a => Type a uni () -> Bool
isHelpType Map Name (Type TyName DefaultUni ())
ctx of
    []         -> Maybe Name
forall a. Maybe a
Nothing
    (Name
x, Type TyName DefaultUni ()
_) : [(Name, Type TyName DefaultUni ())]
_ -> Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x
  where
    isHelpType :: Type a uni () -> Bool
isHelpType (TyForall ()
_ a
x (Type ()) (TyVar ()
_ a
x')) = a
x a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
x'
    isHelpType Type a uni ()
_                                     = Bool
False

mkHelp :: Map Name (Type TyName DefaultUni ())
       -> Type TyName DefaultUni ()
       -> Term TyName Name DefaultUni DefaultFun ()
mkHelp :: Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
mkHelp Map Name (Type TyName DefaultUni ())
_ (TyBuiltin ()
_ SomeTypeIn DefaultUni
someUni)    = SomeTypeIn DefaultUni -> Term TyName Name DefaultUni DefaultFun ()
minimalBuiltin SomeTypeIn DefaultUni
someUni
mkHelp (Map Name (Type TyName DefaultUni ()) -> Maybe Name
findHelp -> Just Name
help) Type TyName DefaultUni ()
ty = ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () (() -> Name -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> name -> Term tyname name uni fun a
Var () Name
help) Type TyName DefaultUni ()
ty
mkHelp Map Name (Type TyName DefaultUni ())
_ Type TyName DefaultUni ()
ty                       = ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> Type tyname uni a -> Term tyname name uni fun a
Error () Type TyName DefaultUni ()
ty

-- | Try to take a term from an old context to a new context and a new type.
-- If we can't do the new type we might return a different type.
fixupTerm_ :: TypeCtx
           -> Map Name (Type TyName DefaultUni ())
           -> TypeCtx
           -> Map Name (Type TyName DefaultUni ())
           -> Type TyName DefaultUni ()
           -> Term TyName Name DefaultUni DefaultFun ()
           -> (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctxOld Map Name (Type TyName DefaultUni ())
ctxOld TypeCtx
tyctxNew Map Name (Type TyName DefaultUni ())
ctxNew Type TyName DefaultUni ()
tyNew Term TyName Name DefaultUni DefaultFun ()
tm0 =
  case TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Either String (Type TyName DefaultUni ())
inferTypeInContext TypeCtx
tyctxNew Map Name (Type TyName DefaultUni ())
ctxNew Term TyName Name DefaultUni DefaultFun ()
tm0 of
    Left String
_ -> case Term TyName Name DefaultUni DefaultFun ()
tm0 of
      -- Make @a@ the new type of @x@. We can't take the old type of @x@, because it may reference
      -- a removed binding. And we're trying to change the type of @tm0@ to @tyNew@ anyway.
      LamAbs ()
_ Name
x Type TyName DefaultUni ()
_ Term TyName Name DefaultUni DefaultFun ()
tm | TyFun () Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b <- Type TyName DefaultUni ()
tyNew -> (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
a) (()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs () Name
x Type TyName DefaultUni ()
a)
                                              ((Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctxOld (Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a Map Name (Type TyName DefaultUni ())
ctxOld)
                                                           TypeCtx
tyctxNew (Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a Map Name (Type TyName DefaultUni ())
ctxNew) Type TyName DefaultUni ()
b Term TyName Name DefaultUni DefaultFun ()
tm
      Apply ()
_ (Apply ()
_ (TyInst ()
_ (Builtin ()
_ DefaultFun
Trace) Type TyName DefaultUni ()
_) Term TyName Name DefaultUni DefaultFun ()
s) Term TyName Name DefaultUni DefaultFun ()
tm ->
        let (Type TyName DefaultUni ()
ty', Term TyName Name DefaultUni DefaultFun ()
tm') = TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctxOld Map Name (Type TyName DefaultUni ())
ctxOld TypeCtx
tyctxNew Map Name (Type TyName DefaultUni ())
ctxNew Type TyName DefaultUni ()
tyNew Term TyName Name DefaultUni DefaultFun ()
tm
        in (Type TyName DefaultUni ()
ty', ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () (()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () (() -> DefaultFun -> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> fun -> Term tyname name uni fun a
Builtin () DefaultFun
Trace) Type TyName DefaultUni ()
ty') Term TyName Name DefaultUni DefaultFun ()
s) Term TyName Name DefaultUni DefaultFun ()
tm')
      Term TyName Name DefaultUni DefaultFun ()
_ | TyBuiltin ()
_ SomeTypeIn DefaultUni
someUni <- Type TyName DefaultUni ()
tyNew -> (Type TyName DefaultUni ()
tyNew, SomeTypeIn DefaultUni -> Term TyName Name DefaultUni DefaultFun ()
minimalBuiltin SomeTypeIn DefaultUni
someUni)
        | Bool
otherwise -> (Type TyName DefaultUni ()
tyNew, Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
mkHelp Map Name (Type TyName DefaultUni ())
ctxNew Type TyName DefaultUni ()
tyNew)
    Right Type TyName DefaultUni ()
ty -> (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm0)

-- | Try to take a term from an old context to a new context and a new type - default to `mkHelp`.
fixupTerm :: TypeCtx
          -> Map Name (Type TyName DefaultUni ())
          -> TypeCtx
          -> Map Name (Type TyName DefaultUni ())
          -> Type TyName DefaultUni ()
          -> Term TyName Name DefaultUni DefaultFun ()
          -> Term TyName Name DefaultUni DefaultFun ()
fixupTerm :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm TypeCtx
_ Map Name (Type TyName DefaultUni ())
_ TypeCtx
tyctxNew Map Name (Type TyName DefaultUni ())
ctxNew Type TyName DefaultUni ()
tyNew Term TyName Name DefaultUni DefaultFun ()
tm
  | Either String () -> Bool
forall a b. Either a b -> Bool
isRight (TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Either String ()
typeCheckTermInContext TypeCtx
tyctxNew Map Name (Type TyName DefaultUni ())
ctxNew Term TyName Name DefaultUni DefaultFun ()
tm Type TyName DefaultUni ()
tyNew) = Term TyName Name DefaultUni DefaultFun ()
tm
  | Bool
otherwise                                                 = Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
mkHelp Map Name (Type TyName DefaultUni ())
ctxNew Type TyName DefaultUni ()
tyNew

minimalBuiltin :: SomeTypeIn DefaultUni -> Term TyName Name DefaultUni DefaultFun ()
minimalBuiltin :: SomeTypeIn DefaultUni -> Term TyName Name DefaultUni DefaultFun ()
minimalBuiltin (SomeTypeIn DefaultUni (Esc a)
uni) = case DefaultUni (Esc a) -> SingKind k
forall k (a :: k). DefaultUni (Esc a) -> SingKind k
forall (uni :: * -> *) k (a :: k).
ToKind uni =>
uni (Esc a) -> SingKind k
toSingKind DefaultUni (Esc a)
uni of
    SingKind k
SingType -> ()
-> DefaultUni (Esc a)
-> a
-> Term TyName Name DefaultUni DefaultFun ()
forall a (uni :: * -> *) fun (term :: * -> *) tyname name ann.
TermLike term tyname name uni fun =>
ann -> uni (Esc a) -> a -> term ann
mkConstantOf () DefaultUni (Esc a)
DefaultUni (Esc a)
uni (a -> Term TyName Name DefaultUni DefaultFun ())
-> a -> Term TyName Name DefaultUni DefaultFun ()
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a) -> a
forall a. DefaultUni (Esc a) -> a
go DefaultUni (Esc a)
DefaultUni (Esc a)
uni
    SingKind k
_        -> String -> Term TyName Name DefaultUni DefaultFun ()
forall a. HasCallStack => String -> a
error String
"Higher-kinded built-in types cannot be used here"
  where
    go :: DefaultUni (Esc a) -> a
    go :: forall a. DefaultUni (Esc a) -> a
go DefaultUni (Esc a)
DefaultUniUnit                                                   = ()
    go DefaultUni (Esc a)
DefaultUniInteger                                                = a
0
    go DefaultUni (Esc a)
DefaultUniBool                                                   = a
Bool
False
    go DefaultUni (Esc a)
DefaultUniString                                                 = a
""
    go DefaultUni (Esc a)
DefaultUniByteString                                             = a
""
    go DefaultUni (Esc a)
DefaultUniData                                                   = Integer -> Data
I Integer
0
    go (DefaultUni (Esc f)
DefaultUniProtoList `DefaultUniApply` DefaultUni (Esc a1)
_)                        = []
    go (DefaultUni (Esc f)
DefaultUniProtoPair `DefaultUniApply` DefaultUni (Esc a1)
a `DefaultUniApply` DefaultUni (Esc a1)
b)    = (DefaultUni (Esc a1) -> a1
forall a. DefaultUni (Esc a) -> a
go DefaultUni (Esc a1)
DefaultUni (Esc a1)
a, DefaultUni (Esc a1) -> a1
forall a. DefaultUni (Esc a) -> a
go DefaultUni (Esc a1)
DefaultUni (Esc a1)
b)
    go (DefaultUni (Esc f)
f  `DefaultUniApply` DefaultUni (Esc a1)
_ `DefaultUniApply` DefaultUni (Esc a1)
_ `DefaultUniApply` DefaultUni (Esc a1)
_) = DefaultUni (Esc f) -> a
forall a b c d (f :: a -> b -> c -> d) any.
DefaultUni (Esc f) -> any
noMoreTypeFunctions DefaultUni (Esc f)
DefaultUni (Esc f)
f
    go DefaultUni (Esc a)
DefaultUniBLS12_381_G1_Element                                   = a
Element
BLS12_381.G1.offchain_zero
    go DefaultUni (Esc a)
DefaultUniBLS12_381_G2_Element                                   = a
Element
BLS12_381.G2.offchain_zero
    go DefaultUni (Esc a)
DefaultUniBLS12_381_MlResult                                     = a
MlResult
BLS12_381.Pairing.identityMlResult

shrinkBind :: HasCallStack
           => Recursivity
           -> TypeCtx
           -> Map Name (Type TyName DefaultUni ())
           -> Binding TyName Name DefaultUni DefaultFun ()
           -> [Binding TyName Name DefaultUni DefaultFun ()]
shrinkBind :: HasCallStack =>
Recursivity
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
shrinkBind Recursivity
_ TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Binding TyName Name DefaultUni DefaultFun ()
bind =
  case Binding TyName Name DefaultUni DefaultFun ()
bind of
    -- Note: this is a bit tricky for recursive binds, if we change a recursive bind we need to
    -- fixup all the other binds in the block. Currently we do this with a fixupTerm_ in the
    -- structural part of shrinking.  In the future this can be made better if we find properties
    -- where lets don't shrink well enough to be understandable.
    TermBind ()
_ Strictness
s (VarDecl ()
_ Name
x Type TyName DefaultUni ()
ty) Term TyName Name DefaultUni DefaultFun ()
tm -> [ ()
-> Strictness
-> VarDecl TyName Name DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Binding TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind () Strictness
s (()
-> Name
-> Type TyName DefaultUni ()
-> VarDecl TyName Name DefaultUni ()
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl () Name
x Type TyName DefaultUni ()
ty') Term TyName Name DefaultUni DefaultFun ()
tm'
                                        | (Type TyName DefaultUni ()
ty', Term TyName Name DefaultUni DefaultFun ()
tm') <- HasCallStack =>
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
shrinkTypedTerm TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm)
                                        ] [Binding TyName Name DefaultUni DefaultFun ()]
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> [Binding TyName Name DefaultUni DefaultFun ()]
forall a. [a] -> [a] -> [a]
++
                                        [ ()
-> Strictness
-> VarDecl TyName Name DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Binding TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Strictness
-> VarDecl tyname name uni a
-> Term tyname name uni fun a
-> Binding tyname name uni fun a
TermBind () Strictness
Strict (()
-> Name
-> Type TyName DefaultUni ()
-> VarDecl TyName Name DefaultUni ()
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl () Name
x Type TyName DefaultUni ()
ty) Term TyName Name DefaultUni DefaultFun ()
tm | Strictness
s Strictness -> Strictness -> Bool
forall a. Eq a => a -> a -> Bool
== Strictness
NonStrict ]
    -- These cases are basically just structural
    TypeBind ()
_ (TyVarDecl ()
_ TyName
a Kind ()
k) Type TyName DefaultUni ()
ty  -> [ ()
-> TyVarDecl TyName ()
-> Type TyName DefaultUni ()
-> Binding TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> TyVarDecl tyname a
-> Type tyname uni a
-> Binding tyname name uni fun a
TypeBind () (() -> TyName -> Kind () -> TyVarDecl TyName ()
forall tyname ann.
ann -> tyname -> Kind ann -> TyVarDecl tyname ann
TyVarDecl () TyName
a Kind ()
k') Type TyName DefaultUni ()
ty'
                                        | (Kind ()
k', Type TyName DefaultUni ()
ty') <- HasCallStack =>
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
shrinkKindAndType TypeCtx
tyctx (Kind ()
k, Type TyName DefaultUni ()
ty) ]
    DatatypeBind ()
_ Datatype TyName Name DefaultUni ()
dat               -> [ ()
-> Datatype TyName Name DefaultUni ()
-> Binding TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> Datatype tyname name uni a -> Binding tyname name uni fun a
DatatypeBind () Datatype TyName Name DefaultUni ()
dat' | Datatype TyName Name DefaultUni ()
dat' <- TypeCtx
-> Datatype TyName Name DefaultUni ()
-> [Datatype TyName Name DefaultUni ()]
shrinkDat TypeCtx
tyctx Datatype TyName Name DefaultUni ()
dat ]

shrinkDat :: TypeCtx
          -> Datatype TyName Name DefaultUni ()
          -> [Datatype TyName Name DefaultUni ()]
shrinkDat :: TypeCtx
-> Datatype TyName Name DefaultUni ()
-> [Datatype TyName Name DefaultUni ()]
shrinkDat TypeCtx
ctx (Datatype ()
_ dd :: TyVarDecl TyName ()
dd@(TyVarDecl ()
_ TyName
d Kind ()
_) [TyVarDecl TyName ()]
xs Name
m [VarDecl TyName Name DefaultUni ()]
cs) =
  [ ()
-> TyVarDecl TyName ()
-> [TyVarDecl TyName ()]
-> Name
-> [VarDecl TyName Name DefaultUni ()]
-> Datatype TyName Name DefaultUni ()
forall tyname name (uni :: * -> *) a.
a
-> TyVarDecl tyname a
-> [TyVarDecl tyname a]
-> name
-> [VarDecl tyname name uni a]
-> Datatype tyname name uni a
Datatype () TyVarDecl TyName ()
dd [TyVarDecl TyName ()]
xs Name
m [VarDecl TyName Name DefaultUni ()]
cs' | [VarDecl TyName Name DefaultUni ()]
cs' <- (VarDecl TyName Name DefaultUni ()
 -> [VarDecl TyName Name DefaultUni ()])
-> [VarDecl TyName Name DefaultUni ()]
-> [[VarDecl TyName Name DefaultUni ()]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList VarDecl TyName Name DefaultUni ()
-> [VarDecl TyName Name DefaultUni ()]
shrinkCon [VarDecl TyName Name DefaultUni ()]
cs ]
  where
    ctx' :: TypeCtx
ctx' = TypeCtx
ctx TypeCtx -> TypeCtx -> TypeCtx
forall a. Semigroup a => a -> a -> a
<> [(TyName, Kind ())] -> TypeCtx
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [ (TyName
x, Kind ()
k) | TyVarDecl ()
_ TyName
x Kind ()
k <- [TyVarDecl TyName ()]
xs ]
    shrinkCon :: VarDecl TyName Name DefaultUni ()
-> [VarDecl TyName Name DefaultUni ()]
shrinkCon (VarDecl ()
_ Name
c Type TyName DefaultUni ()
ty) = [ ()
-> Name
-> Type TyName DefaultUni ()
-> VarDecl TyName Name DefaultUni ()
forall tyname name (uni :: * -> *) ann.
ann -> name -> Type tyname uni ann -> VarDecl tyname name uni ann
VarDecl () Name
c Type TyName DefaultUni ()
ty''
                                 | Type TyName DefaultUni ()
ty' <- HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType TypeCtx
ctx' Type TyName DefaultUni ()
ty
                                 , let ty'' :: Type TyName DefaultUni ()
ty'' = Type TyName DefaultUni ()
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall {tyname} {uni :: * -> *}.
Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
setTarget (Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall {tyname} {uni :: * -> *} {ann}.
Type tyname uni ann -> Type tyname uni ann
getTarget Type TyName DefaultUni ()
ty) Type TyName DefaultUni ()
ty'
                                 , Type TyName DefaultUni ()
ty'' Type TyName DefaultUni () -> Type TyName DefaultUni () -> Bool
forall a. Eq a => a -> a -> Bool
/= Type TyName DefaultUni ()
ty
                                 , TyName
d TyName -> Set TyName -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Getting (Set TyName) (Type TyName DefaultUni ()) TyName
-> Type TyName DefaultUni () -> Set TyName
forall a s. Getting (Set a) s a -> s -> Set a
setOf Getting (Set TyName) (Type TyName DefaultUni ()) TyName
forall tyname unique (uni :: * -> *) ann.
HasUnique tyname unique =>
Traversal' (Type tyname uni ann) tyname
Traversal' (Type TyName DefaultUni ()) TyName
ftvTy (Type TyName DefaultUni ()
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall {tyname} {uni :: * -> *}.
Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
setTarget (forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @() ()) Type TyName DefaultUni ()
ty') ]
      where
        getTarget :: Type tyname uni ann -> Type tyname uni ann
getTarget (TyFun ann
_ Type tyname uni ann
_ Type tyname uni ann
b) = Type tyname uni ann -> Type tyname uni ann
getTarget Type tyname uni ann
b
        getTarget Type tyname uni ann
b             = Type tyname uni ann
b
        setTarget :: Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
setTarget Type tyname uni ()
t (TyFun ()
_ Type tyname uni ()
a Type tyname uni ()
b) = ()
-> Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type tyname uni ()
a (Type tyname uni () -> Type tyname uni () -> Type tyname uni ()
setTarget Type tyname uni ()
t Type tyname uni ()
b)
        setTarget Type tyname uni ()
t Type tyname uni ()
_             = Type tyname uni ()
t

{-
TODO: Note

nonstructural cases for

    let x1 = y1
        x2 = y2
    in b

1. drop all bindings
2. drop body and pick one binding as a new body and drop all bindings appearing after it
3. drop a single binding if there are more than one (because we handled a single one in 1)
-}

{-
TODO: Note

document terms giving duplicate shrinks like

a -> a
let x = "abc" in "abc"
let x = "abc" in x
(\a1_1 -> a1_1) unit
-}

-- | Shrink a typed term in a type and term context.
-- NOTE: if you want to understand what's going on in this function it's a good
-- idea to look at how we do this for types first (it's a lot simpler).
shrinkTypedTerm :: HasCallStack
                => TypeCtx
                -> Map Name (Type TyName DefaultUni ())
                -> (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
                -> [(Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())]
shrinkTypedTerm :: HasCallStack =>
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
shrinkTypedTerm TypeCtx
tyctx0 Map Name (Type TyName DefaultUni ())
ctx0 (Type TyName DefaultUni ()
ty0, Term TyName Name DefaultUni DefaultFun ()
tm0) = [[(Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())]]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    [ -- TODO: this somehow contributes a huge number of duplicates as reported by the @numShrink@
      -- test. How come? Is it because it's called from 'shrinkBind'? Do we even need this kind of
      -- shrinking?
      ((Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())
 -> Bool)
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a. (a -> Bool) -> [a] -> [a]
filter (TypeCtx
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> Bool
scopeCheckTyVars TypeCtx
tyctx0)
        [ (Type TyName DefaultUni ()
ty', Term TyName Name DefaultUni DefaultFun ()
tm')
        | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun () -> Bool
forall {tyname} {uni :: * -> *} {fun} {a}.
Map Name (Type TyName DefaultUni ())
-> Term tyname Name uni fun a -> Bool
isHelp Map Name (Type TyName DefaultUni ())
ctx0 Term TyName Name DefaultUni DefaultFun ()
tm0
        , Type TyName DefaultUni ()
ty' <- Type TyName DefaultUni ()
ty0 Type TyName DefaultUni ()
-> [Type TyName DefaultUni ()] -> [Type TyName DefaultUni ()]
forall a. a -> [a] -> [a]
: HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType (TypeCtx
tyctx0 TypeCtx -> TypeCtx -> TypeCtx
forall a. Semigroup a => a -> a -> a
<> [(TyName, Kind ())] -> TypeCtx
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList (Term TyName Name DefaultUni DefaultFun () -> [(TyName, Kind ())]
datatypes Term TyName Name DefaultUni DefaultFun ()
tm0)) Type TyName DefaultUni ()
ty0
        , let tm' :: Term TyName Name DefaultUni DefaultFun ()
tm' = Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
mkHelp Map Name (Type TyName DefaultUni ())
ctx0 Type TyName DefaultUni ()
ty'
        ]
    , HasCallStack =>
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctx0 Map Name (Type TyName DefaultUni ())
ctx0 (Type TyName DefaultUni ()
ty0, Term TyName Name DefaultUni DefaultFun ()
tm0)
    ]
  where
    isHelp :: Map Name (Type TyName DefaultUni ())
-> Term tyname Name uni fun a -> Bool
isHelp Map Name (Type TyName DefaultUni ())
_ (Constant a
_ Some (ValueOf uni)
_)           = Bool
True
    isHelp Map Name (Type TyName DefaultUni ())
ctx (TyInst a
_ (Var a
_ Name
x) Type tyname uni a
_) = Name -> Maybe Name
forall a. a -> Maybe a
Just Name
x Maybe Name -> Maybe Name -> Bool
forall a. Eq a => a -> a -> Bool
== Map Name (Type TyName DefaultUni ()) -> Maybe Name
findHelp Map Name (Type TyName DefaultUni ())
ctx
    isHelp Map Name (Type TyName DefaultUni ())
_ (Error a
_ Type tyname uni a
_)              = Bool
True
    isHelp Map Name (Type TyName DefaultUni ())
_ Term tyname Name uni fun a
_                        = Bool
False

    addTyBind :: Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind (TypeBind a
_ (TyVarDecl a
_ k
a Kind a
k) Type k uni a
_)                      = k -> Kind a -> Map k (Kind a) -> Map k (Kind a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
a Kind a
k
    addTyBind (DatatypeBind a
_ (Datatype a
_ (TyVarDecl a
_ k
a Kind a
k) [TyVarDecl k a]
_ name
_ [VarDecl k name uni a]
_)) = k -> Kind a -> Map k (Kind a) -> Map k (Kind a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
a Kind a
k
    addTyBind Binding k name uni fun a
_                                                     = Map k (Kind a) -> Map k (Kind a)
forall a. a -> a
id

    addTyBindSubst :: Binding k name uni fun a
-> Map k (Type k uni a) -> Map k (Type k uni a)
addTyBindSubst (TypeBind a
_ (TyVarDecl a
_ k
a Kind a
_) Type k uni a
ty) = k -> Type k uni a -> Map k (Type k uni a) -> Map k (Type k uni a)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
a Type k uni a
ty
    addTyBindSubst Binding k name uni fun a
_                                 = Map k (Type k uni a) -> Map k (Type k uni a)
forall a. a -> a
id

    go :: HasCallStack => _
    go :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm) =
      ((Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())
 -> Bool)
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a. (a -> Bool) -> [a] -> [a]
filter (TypeCtx
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> Bool
scopeCheckTyVars TypeCtx
tyctx) ([(Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())]
 -> [(Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())])
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a b. (a -> b) -> a -> b
$
      HasCallStack =>
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
nonstructural TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm) [(Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a. [a] -> [a] -> [a]
++
      TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
structural    TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm)

    -- TODO: what about 'TyInst'?
    -- These are the special cases and "tricks" for shrinking
    nonstructural :: HasCallStack => _
    nonstructural :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
nonstructural TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm) =
      case Term TyName Name DefaultUni DefaultFun ()
tm of
        -- TODO: shrink Rec to NonRec
        Let ()
_ Recursivity
rec NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL Term TyName Name DefaultUni DefaultFun ()
body -> [[(Type TyName DefaultUni (),
   Term TyName Name DefaultUni DefaultFun ())]]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ --
            [ TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctxInner Map Name (Type TyName DefaultUni ())
ctxInner TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
ty Term TyName Name DefaultUni DefaultFun ()
body
            | let tyctxInner :: TypeCtx
tyctxInner  = (Binding TyName Name DefaultUni DefaultFun ()
 -> TypeCtx -> TypeCtx)
-> TypeCtx
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> TypeCtx
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> TypeCtx -> TypeCtx
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind TypeCtx
tyctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL
                  ctxInner :: Map Name (Type TyName DefaultUni ())
ctxInner    = (Binding TyName Name DefaultUni DefaultFun ()
 -> Map Name (Type TyName DefaultUni ())
 -> Map Name (Type TyName DefaultUni ()))
-> Map Name (Type TyName DefaultUni ())
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Map Name (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind Map Name (Type TyName DefaultUni ())
ctx   NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL
            ]
          , -- Make one of the let-bindings the new body dropping the old body and all the
            -- bindings appearing after the chosen binding (we don't need them, since the whole
            -- 'let' is non-recursive and hence the chosen binding can't reference those appearing
            -- after it).
            [ (Type TyName DefaultUni ()
letTy, case [Binding TyName Name DefaultUni DefaultFun ()]
binds of
                -- If there's no bindings before the chosen one, we don't recreate the 'let'.
                []   -> Term TyName Name DefaultUni DefaultFun ()
letTm
                Binding TyName Name DefaultUni DefaultFun ()
b:[Binding TyName Name DefaultUni DefaultFun ()]
bs -> ()
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () Recursivity
NonRec (Binding TyName Name DefaultUni DefaultFun ()
b Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
forall a. a -> [a] -> NonEmpty a
:| [Binding TyName Name DefaultUni DefaultFun ()]
bs) Term TyName Name DefaultUni DefaultFun ()
letTm)
            | (NonEmptyContext [Binding TyName Name DefaultUni DefaultFun ()]
binds [Binding TyName Name DefaultUni DefaultFun ()]
_, TermBind ()
_ Strictness
_ (VarDecl ()
_ Name
_ Type TyName DefaultUni ()
letTy) Term TyName Name DefaultUni DefaultFun ()
letTm) <-
                NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> [(OneHoleContext
       NonEmpty (Binding TyName Name DefaultUni DefaultFun ()),
     Binding TyName Name DefaultUni DefaultFun ())]
forall a. NonEmpty a -> [(OneHoleContext NonEmpty a, a)]
forall (f :: * -> *) a.
Container f =>
f a -> [(OneHoleContext f a, a)]
oneHoleContexts NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL
            , Recursivity
rec Recursivity -> Recursivity -> Bool
forall a. Eq a => a -> a -> Bool
== Recursivity
NonRec
              -- TODO: check that the body is not one of the bound variables?
            ]
          , -- Drop a single binding.
            [ (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (()
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () Recursivity
rec (Binding TyName Name DefaultUni DefaultFun ()
b Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
forall a. a -> [a] -> NonEmpty a
:| [Binding TyName Name DefaultUni DefaultFun ()]
binds'))
              ((Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctxInner Map Name (Type TyName DefaultUni ())
ctxInner TypeCtx
tyctxInner' Map Name (Type TyName DefaultUni ())
ctxInner' Type TyName DefaultUni ()
ty Term TyName Name DefaultUni DefaultFun ()
body
            | (NonEmptyContext [Binding TyName Name DefaultUni DefaultFun ()]
binds0 [Binding TyName Name DefaultUni DefaultFun ()]
binds1, Binding TyName Name DefaultUni DefaultFun ()
_) <- NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> [(OneHoleContext
       NonEmpty (Binding TyName Name DefaultUni DefaultFun ()),
     Binding TyName Name DefaultUni DefaultFun ())]
forall a. NonEmpty a -> [(OneHoleContext NonEmpty a, a)]
forall (f :: * -> *) a.
Container f =>
f a -> [(OneHoleContext f a, a)]
oneHoleContexts NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL,
              let tyctxInner :: TypeCtx
tyctxInner  = (Binding TyName Name DefaultUni DefaultFun ()
 -> TypeCtx -> TypeCtx)
-> TypeCtx
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> TypeCtx
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> TypeCtx -> TypeCtx
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind TypeCtx
tyctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL
                  ctxInner :: Map Name (Type TyName DefaultUni ())
ctxInner    = (Binding TyName Name DefaultUni DefaultFun ()
 -> Map Name (Type TyName DefaultUni ())
 -> Map Name (Type TyName DefaultUni ()))
-> Map Name (Type TyName DefaultUni ())
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Map Name (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind Map Name (Type TyName DefaultUni ())
ctx   NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
bindsL
                  binds :: [Binding TyName Name DefaultUni DefaultFun ()]
binds       = [Binding TyName Name DefaultUni DefaultFun ()]
binds0 [Binding TyName Name DefaultUni DefaultFun ()]
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> [Binding TyName Name DefaultUni DefaultFun ()]
forall a. [a] -> [a] -> [a]
++ [Binding TyName Name DefaultUni DefaultFun ()]
binds1
                  tyctxInner' :: TypeCtx
tyctxInner' = (Binding TyName Name DefaultUni DefaultFun ()
 -> TypeCtx -> TypeCtx)
-> TypeCtx
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> TypeCtx
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> TypeCtx -> TypeCtx
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind TypeCtx
tyctx [Binding TyName Name DefaultUni DefaultFun ()]
binds
                  ctxInner' :: Map Name (Type TyName DefaultUni ())
ctxInner'   = (Binding TyName Name DefaultUni DefaultFun ()
 -> Map Name (Type TyName DefaultUni ())
 -> Map Name (Type TyName DefaultUni ()))
-> Map Name (Type TyName DefaultUni ())
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> Map Name (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind Map Name (Type TyName DefaultUni ())
ctx   [Binding TyName Name DefaultUni DefaultFun ()]
binds
            , Binding TyName Name DefaultUni DefaultFun ()
b:[Binding TyName Name DefaultUni DefaultFun ()]
binds' <- [[Binding TyName Name DefaultUni DefaultFun ()]
binds]
            ]
          ]

        LamAbs ()
_ Name
x Type TyName DefaultUni ()
a Term TyName Name DefaultUni DefaultFun ()
body ->
          [ TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctx (Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a Map Name (Type TyName DefaultUni ())
ctx) TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
b Term TyName Name DefaultUni DefaultFun ()
body
          | TyFun ()
_ Type TyName DefaultUni ()
_ Type TyName DefaultUni ()
b <- [Type TyName DefaultUni ()
ty]
          ]

        -- Drop substerms
        Apply ()
_ Term TyName Name DefaultUni DefaultFun ()
fun Term TyName Name DefaultUni DefaultFun ()
arg -> case TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Either String (Type TyName DefaultUni ())
inferTypeInContext TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Term TyName Name DefaultUni DefaultFun ()
arg of
          Right Type TyName DefaultUni ()
argTy ->
            [ -- Prefer to keep the same type, so that we don't need to change types elsewhere,
              -- which may remove or cover up the culprit.
              (Type TyName DefaultUni ()
ty, TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
ty Term TyName Name DefaultUni DefaultFun ()
arg)
            , (Type TyName DefaultUni ()
ty, TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
ty Term TyName Name DefaultUni DefaultFun ()
fun)
            , -- But support type-changing shrinking as well in case it's 'fixupTerm' that removes
              -- or covers up the culprit.
              (Type TyName DefaultUni ()
argTy, Term TyName Name DefaultUni DefaultFun ()
arg)
            , (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
argTy Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
fun)
            ]
          Left String
err -> String
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a. HasCallStack => String -> a
error (String
 -> [(Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())])
-> String
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a b. (a -> b) -> a -> b
$ String -> String
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlcCondensedErrorClassic String
err

        TyAbs ()
_ TyName
x Kind ()
_ Term TyName Name DefaultUni DefaultFun ()
body ->
          [ TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ (TyName -> Kind () -> TypeCtx -> TypeCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TyName
x Kind ()
k TypeCtx
tyctx) Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
tyInner' Term TyName Name DefaultUni DefaultFun ()
body
          | TyForall ()
_ TyName
y Kind ()
k Type TyName DefaultUni ()
tyInner <- [Type TyName DefaultUni ()
ty]
          , let tyInner' :: Type TyName DefaultUni ()
tyInner' = TyName
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) a.
Eq tyname =>
tyname
-> Type tyname uni a -> Type tyname uni a -> Type tyname uni a
typeSubstClosedType TyName
y (Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
k) Type TyName DefaultUni ()
tyInner
          ]

        -- TODO: allow non-structural shrinking for some of these.
        Var{} -> []
        Constant{} -> []
        Builtin{} -> []
        TyInst{} -> []
        Error{} -> []
        IWrap{} -> []
        Unwrap{} -> []
        PlutusIR.Constr{} -> []
        Case{} -> []

    -- These are the structural (basically homomorphic) cases in shrinking.
    -- They all just try to shrink a single subterm at a time. We also
    -- use fixupTerm to adjust types here in a trick similar to how we shrunk
    -- types above.
    structural :: HasCallStack => _
    structural :: TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
structural TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
tm) =
      case Term TyName Name DefaultUni DefaultFun ()
tm of

        -- TODO: this needs a long, long Note...
        Let ()
_ Recursivity
rec NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds Term TyName Name DefaultUni DefaultFun ()
body ->
          [ (Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substTypeParallel Map TyName (Type TyName DefaultUni ())
subst Type TyName DefaultUni ()
ty', ()
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () Recursivity
rec NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds Term TyName Name DefaultUni DefaultFun ()
body')
          | (Type TyName DefaultUni ()
ty', Term TyName Name DefaultUni DefaultFun ()
body') <- TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctxInner Map Name (Type TyName DefaultUni ())
ctxInner (Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
body) ] [(Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a. [a] -> [a] -> [a]
++
          [ (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
fix ((Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$ (Term TyName Name DefaultUni DefaultFun ()
 -> Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (()
-> Recursivity
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Recursivity
-> NonEmpty (Binding tyname name uni fun a)
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Let () Recursivity
rec NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds') ((Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
                TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctxInner Map Name (Type TyName DefaultUni ())
ctxInner TypeCtx
tyctxInner' Map Name (Type TyName DefaultUni ())
ctxInner' Type TyName DefaultUni ()
ty Term TyName Name DefaultUni DefaultFun ()
body
            | (context :: OneHoleContext
  NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
context@(NonEmptyContext [Binding TyName Name DefaultUni DefaultFun ()]
before [Binding TyName Name DefaultUni DefaultFun ()]
_), Binding TyName Name DefaultUni DefaultFun ()
bind) <- NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> [(OneHoleContext
       NonEmpty (Binding TyName Name DefaultUni DefaultFun ()),
     Binding TyName Name DefaultUni DefaultFun ())]
forall a. NonEmpty a -> [(OneHoleContext NonEmpty a, a)]
forall (f :: * -> *) a.
Container f =>
f a -> [(OneHoleContext f a, a)]
oneHoleContexts NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds,
              let ctxBind :: Map Name (Type TyName DefaultUni ())
ctxBind | Recursivity
Rec <- Recursivity
rec = Map Name (Type TyName DefaultUni ())
ctxInner
                          | Bool
otherwise  = (Binding TyName Name DefaultUni DefaultFun ()
 -> Map Name (Type TyName DefaultUni ())
 -> Map Name (Type TyName DefaultUni ()))
-> Map Name (Type TyName DefaultUni ())
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> Map Name (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind Map Name (Type TyName DefaultUni ())
ctx [Binding TyName Name DefaultUni DefaultFun ()]
before
                  tyctxBind :: TypeCtx
tyctxBind | Recursivity
Rec <- Recursivity
rec = TypeCtx
tyctxInner
                            | Bool
otherwise  = (Binding TyName Name DefaultUni DefaultFun ()
 -> TypeCtx -> TypeCtx)
-> TypeCtx
-> [Binding TyName Name DefaultUni DefaultFun ()]
-> TypeCtx
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> TypeCtx -> TypeCtx
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind TypeCtx
tyctx [Binding TyName Name DefaultUni DefaultFun ()]
before,
              Binding TyName Name DefaultUni DefaultFun ()
bind' <- HasCallStack =>
Recursivity
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
Recursivity
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Binding TyName Name DefaultUni DefaultFun ()
-> [Binding TyName Name DefaultUni DefaultFun ()]
shrinkBind Recursivity
rec TypeCtx
tyctxBind Map Name (Type TyName DefaultUni ())
ctxBind Binding TyName Name DefaultUni DefaultFun ()
bind,
              let binds' :: NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds'      = OneHoleContext
  NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Binding TyName Name DefaultUni DefaultFun ()
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
forall a. OneHoleContext NonEmpty a -> a -> NonEmpty a
forall (f :: * -> *) a.
Container f =>
OneHoleContext f a -> a -> f a
plugHole OneHoleContext
  NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
context Binding TyName Name DefaultUni DefaultFun ()
bind'
                  tyctxInner' :: TypeCtx
tyctxInner' = (Binding TyName Name DefaultUni DefaultFun ()
 -> TypeCtx -> TypeCtx)
-> TypeCtx
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> TypeCtx
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> TypeCtx -> TypeCtx
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind TypeCtx
tyctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds'
                  ctxInner' :: Map Name (Type TyName DefaultUni ())
ctxInner'   = (Binding TyName Name DefaultUni DefaultFun ()
 -> Map Name (Type TyName DefaultUni ())
 -> Map Name (Type TyName DefaultUni ()))
-> Map Name (Type TyName DefaultUni ())
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Map Name (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind Map Name (Type TyName DefaultUni ())
ctx   NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds'
                  fix :: (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
fix = (Type TyName DefaultUni ()
 -> Term TyName Name DefaultUni DefaultFun ()
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx)
          ] where subst :: Map TyName (Type TyName DefaultUni ())
subst = (Binding TyName Name DefaultUni DefaultFun ()
 -> Map TyName (Type TyName DefaultUni ())
 -> Map TyName (Type TyName DefaultUni ()))
-> Map TyName (Type TyName DefaultUni ())
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Map TyName (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map TyName (Type TyName DefaultUni ())
-> Map TyName (Type TyName DefaultUni ())
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a
-> Map k (Type k uni a) -> Map k (Type k uni a)
addTyBindSubst Map TyName (Type TyName DefaultUni ())
forall a. Monoid a => a
mempty NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds
                  tyctxInner :: TypeCtx
tyctxInner = (Binding TyName Name DefaultUni DefaultFun ()
 -> TypeCtx -> TypeCtx)
-> TypeCtx
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> TypeCtx
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun () -> TypeCtx -> TypeCtx
forall {k} {name} {uni :: * -> *} {fun} {a}.
Ord k =>
Binding k name uni fun a -> Map k (Kind a) -> Map k (Kind a)
addTyBind TypeCtx
tyctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds
                  ctxInner :: Map Name (Type TyName DefaultUni ())
ctxInner   = (Binding TyName Name DefaultUni DefaultFun ()
 -> Map Name (Type TyName DefaultUni ())
 -> Map Name (Type TyName DefaultUni ()))
-> Map Name (Type TyName DefaultUni ())
-> NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
-> Map Name (Type TyName DefaultUni ())
forall a b. (a -> b -> b) -> b -> NonEmpty a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Binding TyName Name DefaultUni DefaultFun ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
addTmBind Map Name (Type TyName DefaultUni ())
ctx NonEmpty (Binding TyName Name DefaultUni DefaultFun ())
binds

        TyInst ()
_ Term TyName Name DefaultUni DefaultFun ()
fun Type TyName DefaultUni ()
argTy -> case TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Either String (Type TyName DefaultUni ())
inferTypeInContext TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Term TyName Name DefaultUni DefaultFun ()
fun of
          Right funTy :: Type TyName DefaultUni ()
funTy@(TyForall ()
_ TyName
x Kind ()
k Type TyName DefaultUni ()
tyInner) ->
            [ (HasCallStack =>
Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substType (TyName
-> Type TyName DefaultUni ()
-> Map TyName (Type TyName DefaultUni ())
forall k a. k -> a -> Map k a
Map.singleton TyName
x' Type TyName DefaultUni ()
argTy') Type TyName DefaultUni ()
tyInner', ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () Term TyName Name DefaultUni DefaultFun ()
fun' Type TyName DefaultUni ()
argTy')
            | (TyForall () TyName
x' Kind ()
k' Type TyName DefaultUni ()
tyInner', Term TyName Name DefaultUni DefaultFun ()
fun') <- TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
funTy, Term TyName Name DefaultUni DefaultFun ()
fun)
            , let argTy' :: Type TyName DefaultUni ()
argTy' | Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== Kind ()
k' = Type TyName DefaultUni ()
argTy
                         -- TODO: define and use proper fixupType
                         | Bool
otherwise = Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
k'
            ] [(Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a. [a] -> [a] -> [a]
++
            [ (HasCallStack =>
Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substType (TyName
-> Type TyName DefaultUni ()
-> Map TyName (Type TyName DefaultUni ())
forall k a. k -> a -> Map k a
Map.singleton TyName
x Type TyName DefaultUni ()
argTy') Type TyName DefaultUni ()
tyInner', ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Type tyname uni a
-> Term tyname name uni fun a
TyInst () Term TyName Name DefaultUni DefaultFun ()
fun' Type TyName DefaultUni ()
argTy')
            | (Kind ()
k', Type TyName DefaultUni ()
argTy') <- HasCallStack =>
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
shrinkKindAndType TypeCtx
tyctx (Kind ()
k, Type TyName DefaultUni ()
argTy)
            , let tyInner' :: Type TyName DefaultUni ()
tyInner' | Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== Kind ()
k'   = Type TyName DefaultUni ()
tyInner
                           -- TODO: define and use proper fixupType
                           | Bool
otherwise = HasCallStack =>
Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
Map TyName (Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
substType (TyName
-> Type TyName DefaultUni ()
-> Map TyName (Type TyName DefaultUni ())
forall k a. k -> a -> Map k a
Map.singleton TyName
x (Type TyName DefaultUni ()
 -> Map TyName (Type TyName DefaultUni ()))
-> Type TyName DefaultUni ()
-> Map TyName (Type TyName DefaultUni ())
forall a b. (a -> b) -> a -> b
$ Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
k) Type TyName DefaultUni ()
tyInner
                  fun' :: Term TyName Name DefaultUni DefaultFun ()
fun' = TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
x Kind ()
k' Type TyName DefaultUni ()
tyInner') Term TyName Name DefaultUni DefaultFun ()
fun
            ]
          Left String
err -> String
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a. HasCallStack => String -> a
error (String
 -> [(Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())])
-> String
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a b. (a -> b) -> a -> b
$ String -> String
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlcCondensedErrorClassic String
err
          Right Type TyName DefaultUni ()
tyWrong -> String
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a. HasCallStack => String -> a
error (String
 -> [(Type TyName DefaultUni (),
      Term TyName Name DefaultUni DefaultFun ())])
-> String
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a b. (a -> b) -> a -> b
$ String
"Expected a 'TyForall', but got " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Type TyName DefaultUni () -> String
forall a str. (PrettyPlc a, Render str) => a -> str
displayPlc Type TyName DefaultUni ()
tyWrong

        -- TODO: shrink the kind too like with the type in @LamAbs@ below.
        TyAbs ()
_ TyName
x Kind ()
_ Term TyName Name DefaultUni DefaultFun ()
body | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ TyName -> TypeCtx -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member TyName
x TypeCtx
tyctx ->
          [ (()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyForall () TyName
x Kind ()
k Type TyName DefaultUni ()
tyInner', ()
-> TyName
-> Kind ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> tyname
-> Kind a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
TyAbs () TyName
x Kind ()
k Term TyName Name DefaultUni DefaultFun ()
body')
          | TyForall ()
_ TyName
y Kind ()
k Type TyName DefaultUni ()
tyInner <- [Type TyName DefaultUni ()
ty]
          , (Type TyName DefaultUni ()
tyInner', Term TyName Name DefaultUni DefaultFun ()
body') <- TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
go (TyName -> Kind () -> TypeCtx -> TypeCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TyName
x Kind ()
k TypeCtx
tyctx) Map Name (Type TyName DefaultUni ())
ctx (TyName
-> TyName -> Type TyName DefaultUni () -> Type TyName DefaultUni ()
renameVar TyName
y TyName
x Type TyName DefaultUni ()
tyInner, Term TyName Name DefaultUni DefaultFun ()
body)
          ]

        LamAbs ()
_ Name
x Type TyName DefaultUni ()
a Term TyName Name DefaultUni DefaultFun ()
body ->
          [ (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b', ()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs () Name
x Type TyName DefaultUni ()
a Term TyName Name DefaultUni DefaultFun ()
body')
          | TyFun ()
_ Type TyName DefaultUni ()
_ Type TyName DefaultUni ()
b <- [Type TyName DefaultUni ()
ty],
            (Type TyName DefaultUni ()
b', Term TyName Name DefaultUni DefaultFun ()
body') <- TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctx (Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a Map Name (Type TyName DefaultUni ())
ctx) (Type TyName DefaultUni ()
b, Term TyName Name DefaultUni DefaultFun ()
body)
          ] [(Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a. [a] -> [a] -> [a]
++
          [ (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> (Term TyName Name DefaultUni DefaultFun ()
    -> Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
a') (()
-> Name
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> name
-> Type tyname uni a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
LamAbs () Name
x Type TyName DefaultUni ()
a') ((Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())
 -> (Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ()))
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
forall a b. (a -> b) -> a -> b
$
              TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
fixupTerm_ TypeCtx
tyctx (Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a Map Name (Type TyName DefaultUni ())
ctx) TypeCtx
tyctx (Name
-> Type TyName DefaultUni ()
-> Map Name (Type TyName DefaultUni ())
-> Map Name (Type TyName DefaultUni ())
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Name
x Type TyName DefaultUni ()
a' Map Name (Type TyName DefaultUni ())
ctx) Type TyName DefaultUni ()
b Term TyName Name DefaultUni DefaultFun ()
body
          | TyFun ()
_ Type TyName DefaultUni ()
_ Type TyName DefaultUni ()
b <- [Type TyName DefaultUni ()
ty],
            Type TyName DefaultUni ()
a' <- HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType TypeCtx
tyctx Type TyName DefaultUni ()
a
          ]

        Apply ()
_ Term TyName Name DefaultUni DefaultFun ()
fun Term TyName Name DefaultUni DefaultFun ()
arg -> case TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Term TyName Name DefaultUni DefaultFun ()
-> Either String (Type TyName DefaultUni ())
inferTypeInContext TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Term TyName Name DefaultUni DefaultFun ()
arg of
          Left String
err    -> String
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a. HasCallStack => String -> a
error String
err
          Right Type TyName DefaultUni ()
argTy ->
            [ (Type TyName DefaultUni ()
ty', ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () Term TyName Name DefaultUni DefaultFun ()
fun' Term TyName Name DefaultUni DefaultFun ()
arg')
            | (TyFun ()
_ Type TyName DefaultUni ()
argTy' Type TyName DefaultUni ()
ty', Term TyName Name DefaultUni DefaultFun ()
fun') <- TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
argTy Type TyName DefaultUni ()
ty, Term TyName Name DefaultUni DefaultFun ()
fun)
            , let arg' :: Term TyName Name DefaultUni DefaultFun ()
arg' = TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx Type TyName DefaultUni ()
argTy' Term TyName Name DefaultUni DefaultFun ()
arg
            ] [(Type TyName DefaultUni (),
  Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall a. [a] -> [a] -> [a]
++
            [ (Type TyName DefaultUni ()
ty,  ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
-> Term tyname name uni fun a
Apply () Term TyName Name DefaultUni DefaultFun ()
fun' Term TyName Name DefaultUni DefaultFun ()
arg')
            | (Type TyName DefaultUni ()
argTy', Term TyName Name DefaultUni DefaultFun ()
arg') <- TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
go TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (Type TyName DefaultUni ()
argTy, Term TyName Name DefaultUni DefaultFun ()
arg)
            , let fun' :: Term TyName Name DefaultUni DefaultFun ()
fun' = TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
-> Term TyName Name DefaultUni DefaultFun ()
fixupTerm TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx TypeCtx
tyctx Map Name (Type TyName DefaultUni ())
ctx (()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> Type tyname uni ann
-> Type tyname uni ann
-> Type tyname uni ann
TyFun () Type TyName DefaultUni ()
argTy' Type TyName DefaultUni ()
ty) Term TyName Name DefaultUni DefaultFun ()
fun
            ]

        Constant ()
_ Some (ValueOf DefaultUni)
val ->
          Some (ValueOf DefaultUni) -> [Some (ValueOf DefaultUni)]
forall a. Arbitrary a => a -> [a]
shrink Some (ValueOf DefaultUni)
val [Some (ValueOf DefaultUni)]
-> (Some (ValueOf DefaultUni)
    -> (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \val' :: Some (ValueOf DefaultUni)
val'@(Some (ValueOf DefaultUni (Esc a)
uni a
_)) ->
            (() -> DefaultUni (Esc a) -> Type TyName DefaultUni ()
forall k (a :: k) (uni :: * -> *) tyname ann.
ann -> uni (Esc a) -> Type tyname uni ann
mkTyBuiltinOf () DefaultUni (Esc a)
uni, ()
-> Some (ValueOf DefaultUni)
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> Some (ValueOf uni) -> Term tyname name uni fun a
Constant () Some (ValueOf DefaultUni)
val')

        Error ()
_ Type TyName DefaultUni ()
_ -> HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType TypeCtx
tyctx Type TyName DefaultUni ()
ty [Type TyName DefaultUni ()]
-> (Type TyName DefaultUni ()
    -> (Type TyName DefaultUni (),
        Term TyName Name DefaultUni DefaultFun ()))
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Type TyName DefaultUni ()
ty' -> (Type TyName DefaultUni ()
ty', ()
-> Type TyName DefaultUni ()
-> Term TyName Name DefaultUni DefaultFun ()
forall tyname name (uni :: * -> *) fun a.
a -> Type tyname uni a -> Term tyname name uni fun a
Error () Type TyName DefaultUni ()
ty')

        -- TODO: allow structural shrinking for some of these.
        Var{} -> []
        IWrap{} -> []
        Unwrap{} -> []
        Builtin{} -> []
        Case{} -> []
        TyAbs{} -> []
        PlutusIR.Constr{} -> []

shrinkClosedTypedTerm :: (Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())
                      -> [(Type TyName DefaultUni (), Term TyName Name DefaultUni DefaultFun ())]
shrinkClosedTypedTerm :: (Type TyName DefaultUni (),
 Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
shrinkClosedTypedTerm = HasCallStack =>
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
TypeCtx
-> Map Name (Type TyName DefaultUni ())
-> (Type TyName DefaultUni (),
    Term TyName Name DefaultUni DefaultFun ())
-> [(Type TyName DefaultUni (),
     Term TyName Name DefaultUni DefaultFun ())]
shrinkTypedTerm TypeCtx
forall a. Monoid a => a
mempty Map Name (Type TyName DefaultUni ())
forall a. Monoid a => a
mempty