{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}

{-| This module defines the type shrinker. The shrinking order isn't specified, so the shrinker
may or may not behave correctly, we don't really know. If shrinking ever loops, feel free to kill
this module or reverse-engineer the shrinker and fix the problem. -}
module PlutusCore.Generators.QuickCheck.ShrinkTypes where

import PlutusCore.Generators.QuickCheck.Builtin
import PlutusCore.Generators.QuickCheck.Common
import PlutusCore.Generators.QuickCheck.GenTm
import PlutusCore.Generators.QuickCheck.GenerateKinds

import PlutusCore.Builtin
import PlutusCore.Core
import PlutusCore.Default
import PlutusCore.Name.Unique
import PlutusCore.Pretty
import PlutusCore.Subst

import Data.Map.Strict qualified as Map
import Data.Set.Lens (setOf)
import GHC.Stack
import Test.QuickCheck.Arbitrary

{- Note [Avoiding Shrinking Loops]

   Shrinking loops can be tricky to deal with and unfortunately there is no
   golden rule for how to avoid them. However, one good strategy to avoid them
   is to make sure shrinking isn't doing anything too clever. As a general set of
   rules:
   * Don't do "special case" shrinking that trades off size in one subterm for size
     in a different subterm. For example, it's generally dangerous to shrink
     `Node (Node Leaf (Node Leaf Leaf)) (Node Leaf Leaf)` to
     `Node Leaf (Node Leaf (Node Leaf Leaf))` even though the number of leaves is
     decreasing unless you've explicitly made "the number of leaves decreases" the
     measure by which you're shrinking (in which case you need to have a property for
     this!)
   * Carefully guard base cases - the shrinker
     `shrink tree = Leaf : someCleverShrinkingStrategy` will loop, while
     `shrink tree = [ Leaf | tree /= Leaf ] ++ someCleverShrinkingStrategy` will not.
     You will see this kind of thing used below wherever we use `minimalType` and `mkHelp`
     in the shrinkers.
   * Write properties to test your shrinkers and *run them when you change your shrinkers*.
     See e.g. `prop_noTermShrinkLoops` in module `GeneratorSpec`.
-}

-- Note that compared to 'genAtomicType' this one for, say, @* -> * -> *@ always gives @pair@, while
-- 'genAtomicType' can give you a type variable, 'pair' or a type lambda returning a type variable,
-- 'list' or a type lambda returning a type variable or a built-in type of kind @*@.
{-| Give a unique "least" (intentionally vaguely specified by "shrinking order")
type of that kind. Note: this function requires care and attention to not get
a shrinking loop. If you think you need to mess with this function:
0. First, you *must* read the note Note [Avoiding Shrinking Loops]
1. You're probably wrong, think again and
2. If you're sure you're not wrong you need to be very careful and
   test the shrinking to make sure you don't get in a loop.
3. Finally, you *must* read the note Note [Avoiding Shrinking Loops] -}
minimalType :: Kind () -> Type TyName DefaultUni ()
minimalType :: Kind () -> Type TyName DefaultUni ()
minimalType = [Kind ()] -> Type TyName DefaultUni ()
go ([Kind ()] -> Type TyName DefaultUni ())
-> (Kind () -> [Kind ()]) -> Kind () -> Type TyName DefaultUni ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind () -> [Kind ()]
forall ann. Kind ann -> [Kind ann]
argsFunKind
  where
    go :: [Kind ()] -> Type TyName DefaultUni ()
go = \case
      [] -> Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
unit
      [Type {}] -> Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
list
      [Type {}, Type {}] -> Type TyName DefaultUni ()
forall {tyname}. Type tyname DefaultUni ()
pair
      Kind ()
k : [Kind ()]
ks -> ()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () (Name -> TyName
TyName (Name -> TyName) -> Name -> TyName
forall a b. (a -> b) -> a -> b
$ Text -> Unique -> Name
Name Text
"_" (Int -> Unique
forall a. Enum a => Int -> a
toEnum Int
0)) Kind ()
k (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ [Kind ()] -> Type TyName DefaultUni ()
go [Kind ()]
ks

    unit :: Type tyname DefaultUni ()
unit = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @() ()
    list :: Type tyname DefaultUni ()
list = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @[] ()
    pair :: Type tyname DefaultUni ()
pair = forall a (x :: a) (uni :: * -> *) ann tyname.
HasTypeLevel uni x =>
ann -> Type tyname uni ann
mkTyBuiltin @_ @(,) ()

{-| Take a type in a context and a target kind and try adjust the type to have the target kind.
If can't make the adjusting successful, return the 'minimalType' of the target kind.
Precondition: new kind is smaller or equal to old kind of the type.
Complies with the implicit shrinking order.
TODO (later): also allow changing which context it's valid in -}
fixKind
  :: HasCallStack
  => TypeCtx
  -> Type TyName DefaultUni ()
  -> Kind ()
  -> Type TyName DefaultUni ()
fixKind :: HasCallStack =>
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
fixKind TypeCtx
ctx Type TyName DefaultUni ()
ty Kind ()
k
  -- Nothing to do if we already have the right kind
  | Kind ()
origK Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== Kind ()
k = Type TyName DefaultUni ()
ty
  | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Kind ()
k Kind () -> Kind () -> Bool
`leKind` Kind ()
origK =
      [Char] -> Type TyName DefaultUni ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> Type TyName DefaultUni ())
-> [Char] -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$
        [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
          [ [Char]
"Internal error. New kind: "
          , Kind () -> [Char]
forall str a. (Pretty a, Render str) => a -> str
display Kind ()
k
          , [Char]
"\nis not smaller than the old one: "
          , Kind () -> [Char]
forall str a. (Pretty a, Render str) => a -> str
display (Kind () -> [Char]) -> Kind () -> [Char]
forall a b. (a -> b) -> a -> b
$ HasCallStack => TypeCtx -> Type TyName DefaultUni () -> Kind ()
TypeCtx -> Type TyName DefaultUni () -> Kind ()
unsafeInferKind TypeCtx
ctx Type TyName DefaultUni ()
ty
          ]
  | Bool
otherwise = case Type TyName DefaultUni ()
ty of
      -- Switch a variable out for a different variable of the right kind
      TyVar ()
_ TyName
_ -> case [TyName
y | (TyName
y, Kind ()
k') <- TypeCtx -> [(TyName, Kind ())]
forall k a. Map k a -> [(k, a)]
Map.toList TypeCtx
ctx, Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== Kind ()
k'] of
        TyName
y : [TyName]
_ -> () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
y
        [TyName]
_ -> Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
k
      -- Try to fix application by fixing the function
      TyApp ()
_ Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b -> ()
-> 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
TyApp () (HasCallStack =>
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
fixKind TypeCtx
ctx Type TyName DefaultUni ()
a (Kind () -> Type TyName DefaultUni ())
-> Kind () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () (HasCallStack => TypeCtx -> Type TyName DefaultUni () -> Kind ()
TypeCtx -> Type TyName DefaultUni () -> Kind ()
unsafeInferKind TypeCtx
ctx Type TyName DefaultUni ()
b) Kind ()
k) Type TyName DefaultUni ()
b
      TyLam ()
_ TyName
x Kind ()
kx Type TyName DefaultUni ()
b ->
        case Kind ()
k of
          -- Fix lambdas to * by substituting a minimal type for the argument
          -- and fixing the body.
          Type {} -> HasCallStack =>
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
fixKind TypeCtx
ctx (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
x (Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
kx) Type TyName DefaultUni ()
b) Kind ()
k
          -- Fix functions by either keeping the argument around (if we can) or getting
          -- rid of the argument (by turning its use-sites into minimal types) and introducing
          -- a new argument.
          KindArrow ()
_ Kind ()
ka Kind ()
kb
            | Kind ()
ka Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== Kind ()
kx -> ()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
x Kind ()
kx (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
fixKind (TyName -> Kind () -> TypeCtx -> TypeCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TyName
x Kind ()
kx TypeCtx
ctx) Type TyName DefaultUni ()
b Kind ()
kb
            | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Kind ()
kb Kind () -> Kind () -> Bool
`leKind` Kind ()
kb' -> [Char] -> Type TyName DefaultUni ()
forall a. HasCallStack => [Char] -> a
error [Char]
"fixKind"
            | Bool
otherwise -> ()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
x Kind ()
ka (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
fixKind TypeCtx
ctx' Type TyName DefaultUni ()
b' Kind ()
kb
            where
              ctx' :: TypeCtx
ctx' = TyName -> Kind () -> TypeCtx -> TypeCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TyName
x Kind ()
ka TypeCtx
ctx
              b' :: Type TyName DefaultUni ()
b' = 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
x (Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
kx) Type TyName DefaultUni ()
b
              kb' :: Kind ()
kb' = HasCallStack => TypeCtx -> Type TyName DefaultUni () -> Kind ()
TypeCtx -> Type TyName DefaultUni () -> Kind ()
unsafeInferKind TypeCtx
ctx' Type TyName DefaultUni ()
b'
      -- Ill-kinded builtins just go to minimal types
      TyBuiltin {} -> Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
k
      -- Unreachable, because the target kind must be less than or equal to the original kind. We
      -- handled the case where they are equal at the beginning of the function, so at this point the
      -- target kind must be strictly less than the original kind, but for these types we know the
      -- original kind is @*@, and there is no kind smaller than that.
      TyFun {} -> [Char] -> Type TyName DefaultUni ()
forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: unreachable clause."
      TyIFix {} -> [Char] -> Type TyName DefaultUni ()
forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: unreachable clause."
      TyForall {} -> [Char] -> Type TyName DefaultUni ()
forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: unreachable clause."
      TySOP {} -> [Char] -> Type TyName DefaultUni ()
forall a. HasCallStack => [Char] -> a
error [Char]
"Internal error: unreachable clause."
  where
    origK :: Kind ()
origK = HasCallStack => TypeCtx -> Type TyName DefaultUni () -> Kind ()
TypeCtx -> Type TyName DefaultUni () -> Kind ()
unsafeInferKind TypeCtx
ctx Type TyName DefaultUni ()
ty

{-| Shrink a well-kinded type in a context to new types, possibly with new kinds.
The new kinds are guaranteed to be smaller than or equal to the old kind.
TODO: also shrink to new context
      need old context and new context -}
shrinkKindAndType
  :: HasCallStack
  => TypeCtx
  -> (Kind (), Type TyName DefaultUni ())
  -> [(Kind (), Type TyName DefaultUni ())]
shrinkKindAndType :: HasCallStack =>
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
shrinkKindAndType TypeCtx
ctx (Kind ()
k0, Type TyName DefaultUni ()
ty) =
  let minK0 :: Type TyName DefaultUni ()
minK0 = Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
k0
   in -- If we are not already minimal, add the minial type as a possible shrink.
      ([(Kind ()
k0, Type TyName DefaultUni ()
m) | let m :: Type TyName DefaultUni ()
m = Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
k0, Type TyName DefaultUni ()
m Type TyName DefaultUni () -> Type TyName DefaultUni () -> Bool
forall a. Eq a => a -> a -> Bool
/= Type TyName DefaultUni ()
ty] [(Kind (), Type TyName DefaultUni ())]
-> [(Kind (), Type TyName DefaultUni ())]
-> [(Kind (), Type TyName DefaultUni ())]
forall a. [a] -> [a] -> [a]
++) ([(Kind (), Type TyName DefaultUni ())]
 -> [(Kind (), Type TyName DefaultUni ())])
-> ([(Kind (), Type TyName DefaultUni ())]
    -> [(Kind (), Type TyName DefaultUni ())])
-> [(Kind (), Type TyName DefaultUni ())]
-> [(Kind (), Type TyName DefaultUni ())]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Kind (), Type TyName DefaultUni ()) -> Bool)
-> [(Kind (), Type TyName DefaultUni ())]
-> [(Kind (), Type TyName DefaultUni ())]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Type TyName DefaultUni () -> Type TyName DefaultUni () -> Bool
forall a. Eq a => a -> a -> Bool
/= Type TyName DefaultUni ()
minK0) (Type TyName DefaultUni () -> Bool)
-> ((Kind (), Type TyName DefaultUni ())
    -> Type TyName DefaultUni ())
-> (Kind (), Type TyName DefaultUni ())
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind (), Type TyName DefaultUni ()) -> Type TyName DefaultUni ()
forall a b. (a, b) -> b
snd) ([(Kind (), Type TyName DefaultUni ())]
 -> [(Kind (), Type TyName DefaultUni ())])
-> [(Kind (), Type TyName DefaultUni ())]
-> [(Kind (), Type TyName DefaultUni ())]
forall a b. (a -> b) -> a -> b
$
        [(Kind ()
k, Type TyName DefaultUni ()
m) | Kind ()
k <- Kind () -> [Kind ()]
forall a. Arbitrary a => a -> [a]
shrink Kind ()
k0, let m :: Type TyName DefaultUni ()
m = Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
k]
          [(Kind (), Type TyName DefaultUni ())]
-> [(Kind (), Type TyName DefaultUni ())]
-> [(Kind (), Type TyName DefaultUni ())]
forall a. [a] -> [a] -> [a]
++ case Type TyName DefaultUni ()
ty of
            -- Variables shrink to arbitrary "smaller" variables
            -- Note: the order on variable names here doesn't matter,
            -- it's just because we need *some* order or otherwise
            -- shrinking doesn't terminate.
            TyVar ()
_ TyName
x ->
              [ (Kind ()
ky, () -> TyName -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> tyname -> Type tyname uni ann
TyVar () TyName
y)
              | (TyName
y, Kind ()
ky) <- TypeCtx -> [(TyName, Kind ())]
forall k a. Map k a -> [(k, a)]
Map.toList TypeCtx
ctx
              , Kind () -> Kind () -> Bool
ltKind Kind ()
ky Kind ()
k0 Bool -> Bool -> Bool
|| Kind ()
ky Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== Kind ()
k0 Bool -> Bool -> Bool
&& TyName
y TyName -> TyName -> Bool
forall a. Ord a => a -> a -> Bool
< TyName
x
              ]
            -- Functions shrink to either side of the arrow and both sides
            -- of the arrow shrink independently.
            TyFun ()
_ Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b ->
              (Type TyName DefaultUni () -> (Kind (), Type TyName DefaultUni ()))
-> [Type TyName DefaultUni ()]
-> [(Kind (), Type TyName DefaultUni ())]
forall a b. (a -> b) -> [a] -> [b]
map (() -> Kind ()
forall ann. ann -> Kind ann
Type (),) ([Type TyName DefaultUni ()]
 -> [(Kind (), Type TyName DefaultUni ())])
-> [Type TyName DefaultUni ()]
-> [(Kind (), Type TyName DefaultUni ())]
forall a b. (a -> b) -> a -> b
$
                [[Type TyName DefaultUni ()]] -> [Type TyName DefaultUni ()]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                  [
                    [ Type TyName DefaultUni ()
a
                    , Type TyName DefaultUni ()
b
                    ]
                  , [ ()
-> 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
                    | Type TyName DefaultUni ()
a' <- HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType TypeCtx
ctx Type TyName DefaultUni ()
a
                    ]
                  , [ ()
-> 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'
                    | Type TyName DefaultUni ()
b' <- HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType TypeCtx
ctx Type TyName DefaultUni ()
b
                    ]
                  ]
            -- This case needs to be handled with a bit of care. First we shrink applications by
            -- doing simple stuff like shrinking the function and body separately when we can.
            -- The slightly tricky case is the concat trace. See comment below.
            TyApp ()
_ Type TyName DefaultUni ()
f Type TyName DefaultUni ()
a ->
              [[(Kind (), Type TyName DefaultUni ())]]
-> [(Kind (), Type TyName DefaultUni ())]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                [ [ (Kind ()
ka, Type TyName DefaultUni ()
a)
                  | Kind ()
ka Kind () -> Kind () -> Bool
`leKind` Kind ()
k0
                  ]
                , [ (Kind ()
k0, 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
x Type TyName DefaultUni ()
m Type TyName DefaultUni ()
b)
                  | TyLam ()
_ TyName
x Kind ()
_ Type TyName DefaultUni ()
b <- [Type TyName DefaultUni ()
f]
                  , let m :: Type TyName DefaultUni ()
m = Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
ka
                  , Type TyName DefaultUni ()
m Type TyName DefaultUni () -> Type TyName DefaultUni () -> Bool
forall a. Eq a => a -> a -> Bool
/= Type TyName DefaultUni ()
a -- @m == a@ is handled right below.
                  ]
                , [ (Kind ()
k0, 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
x Type TyName DefaultUni ()
a Type TyName DefaultUni ()
b)
                  | TyLam ()
_ TyName
x Kind ()
_ Type TyName DefaultUni ()
b <- [Type TyName DefaultUni ()
f]
                  , Set TyName -> Bool
forall a. Set a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (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 ()
a)
                  ]
                , -- Here we try to shrink the function f, if we get something whose kind
                  -- is small enough we can return the new function f', otherwise we
                  -- apply f' to `fixKind ctx a ka'` - which takes `a` and tries to rewrite it
                  -- to something of kind `ka'`.
                  [[(Kind (), Type TyName DefaultUni ())]]
-> [(Kind (), Type TyName DefaultUni ())]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                    [ case Kind ()
kf' of
                        Type {} ->
                          [ (Kind ()
kf', Type TyName DefaultUni ()
f')
                          | Type TyName DefaultUni ()
f' Type TyName DefaultUni () -> Type TyName DefaultUni () -> Bool
forall a. Eq a => a -> a -> Bool
/= Type TyName DefaultUni ()
a -- @f' == a@ is handled above.
                          ]
                        KindArrow ()
_ Kind ()
ka' Kind ()
kb' ->
                          [ (Kind ()
kb', ()
-> 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
TyApp () Type TyName DefaultUni ()
f' (HasCallStack =>
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
fixKind TypeCtx
ctx Type TyName DefaultUni ()
a Kind ()
ka'))
                          | Kind () -> Kind () -> Bool
leKind Kind ()
kb' Kind ()
k0
                          , Kind () -> Kind () -> Bool
leKind Kind ()
ka' Kind ()
ka
                          ]
                    | (Kind ()
kf', Type TyName DefaultUni ()
f') <- HasCallStack =>
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
shrinkKindAndType TypeCtx
ctx (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
ka Kind ()
k0, Type TyName DefaultUni ()
f)
                    ]
                , -- Here we shrink the argument and fixup the function to have the right kind.
                  [ (Kind ()
k0, ()
-> 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
TyApp () (HasCallStack =>
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
fixKind TypeCtx
ctx Type TyName DefaultUni ()
f (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
ka' Kind ()
k0)) Type TyName DefaultUni ()
a')
                  | (Kind ()
ka', Type TyName DefaultUni ()
a') <- HasCallStack =>
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
shrinkKindAndType TypeCtx
ctx (Kind ()
ka, Type TyName DefaultUni ()
a)
                  ]
                ]
              where
                ka :: Kind ()
ka = HasCallStack => TypeCtx -> Type TyName DefaultUni () -> Kind ()
TypeCtx -> Type TyName DefaultUni () -> Kind ()
unsafeInferKind TypeCtx
ctx Type TyName DefaultUni ()
a
            -- type lambdas shrink by either shrinking the kind of the argument or shrinking the body
            TyLam ()
_ TyName
x Kind ()
ka Type TyName DefaultUni ()
b ->
              [[(Kind (), Type TyName DefaultUni ())]]
-> [(Kind (), Type TyName DefaultUni ())]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                [ -- We can simply get rid of the binding by instantiating the variable.

                  [ (Kind ()
kb, 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
x (Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
ka) Type TyName DefaultUni ()
b)
                  ]
                , -- We could've used @fixKind (Map.insert x ka' ctx) (TyVar () x) ka)@ here instead of
                  -- @minimalType ka@, so that the usages of @x@ are preserved when possible, but that would
                  -- mean fixing a kind to a bigger one (because @ka'@ has to be smaller than @ka@ and we'd go
                  -- in the opposite direction), which is not supported by 'fixKind' (even though just
                  -- commenting out the relevant check and making the change here does seem to give us
                  -- better shrinking that still properly terminates, 'cause why would it not).
                  [ (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
ka' Kind ()
kb, ()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
x Kind ()
ka' (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ 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
x (Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
ka) Type TyName DefaultUni ()
b)
                  | Kind ()
ka' <- Kind () -> [Kind ()]
forall a. Arbitrary a => a -> [a]
shrink Kind ()
ka
                  ]
                , [ (() -> Kind () -> Kind () -> Kind ()
forall ann. ann -> Kind ann -> Kind ann -> Kind ann
KindArrow () Kind ()
ka Kind ()
kb', ()
-> TyName
-> Kind ()
-> Type TyName DefaultUni ()
-> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann
-> tyname -> Kind ann -> Type tyname uni ann -> Type tyname uni ann
TyLam () TyName
x Kind ()
ka Type TyName DefaultUni ()
b')
                  | (Kind ()
kb', Type TyName DefaultUni ()
b') <- HasCallStack =>
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
shrinkKindAndType (TyName -> Kind () -> TypeCtx -> TypeCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TyName
x Kind ()
ka TypeCtx
ctx) (Kind ()
kb, Type TyName DefaultUni ()
b)
                  ]
                ]
              where
                kb :: Kind ()
kb = case Kind ()
k0 of
                  KindArrow ()
_ Kind ()
_ Kind ()
k' -> Kind ()
k'
                  Kind ()
_ ->
                    [Char] -> Kind ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> Kind ()) -> [Char] -> Kind ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Internal error: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Kind () -> [Char]
forall str a. (Pretty a, Render str) => a -> str
display Kind ()
k0 [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" is not a 'KindArrow'"
            TyForall ()
_ TyName
x Kind ()
ka Type TyName DefaultUni ()
b ->
              (Type TyName DefaultUni () -> (Kind (), Type TyName DefaultUni ()))
-> [Type TyName DefaultUni ()]
-> [(Kind (), Type TyName DefaultUni ())]
forall a b. (a -> b) -> [a] -> [b]
map (() -> Kind ()
forall ann. ann -> Kind ann
Type (),) ([Type TyName DefaultUni ()]
 -> [(Kind (), Type TyName DefaultUni ())])
-> [Type TyName DefaultUni ()]
-> [(Kind (), Type TyName DefaultUni ())]
forall a b. (a -> b) -> a -> b
$
                [[Type TyName DefaultUni ()]] -> [Type TyName DefaultUni ()]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                  [ -- We can simply get rid of the binding by instantiating the variable.

                    [ 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
x (Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
ka) Type TyName DefaultUni ()
b
                    ]
                  , -- We can always just shrink the bound variable to a smaller kind and ignore it
                    -- Similarly to 'TyLam', we could've used 'fixKind' here, but we don't do it for the same
                    -- reason.
                    [ ()
-> 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 ()
ka' (Type TyName DefaultUni () -> Type TyName DefaultUni ())
-> Type TyName DefaultUni () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ 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
x (Kind () -> Type TyName DefaultUni ()
minimalType Kind ()
ka) Type TyName DefaultUni ()
b
                    | Kind ()
ka' <- Kind () -> [Kind ()]
forall a. Arbitrary a => a -> [a]
shrink Kind ()
ka
                    ]
                  , [ ()
-> 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 ()
ka Type TyName DefaultUni ()
b'
                    | -- or we shrink the body.
                    Type TyName DefaultUni ()
b' <- HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType (TyName -> Kind () -> TypeCtx -> TypeCtx
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert TyName
x Kind ()
ka TypeCtx
ctx) Type TyName DefaultUni ()
b
                    ]
                  ]
            TyBuiltin ()
_ SomeTypeIn DefaultUni
someUni ->
              [ (DefaultUni (Esc a) -> Kind ()
forall {k} (uni :: * -> *) (a :: k).
ToKind uni =>
uni (Esc a) -> Kind ()
kindOfBuiltinType DefaultUni (Esc a)
uni', () -> SomeTypeIn DefaultUni -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> SomeTypeIn uni -> Type tyname uni ann
TyBuiltin () (SomeTypeIn DefaultUni -> Type TyName DefaultUni ())
-> SomeTypeIn DefaultUni -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ DefaultUni (Esc a) -> SomeTypeIn DefaultUni
forall (uni :: * -> *) k (a :: k). uni (Esc a) -> SomeTypeIn uni
SomeTypeIn DefaultUni (Esc a)
uni')
              | SomeTypeIn DefaultUni (Esc a)
uni' <- SomeTypeIn DefaultUni -> [SomeTypeIn DefaultUni]
shrinkBuiltinType SomeTypeIn DefaultUni
someUni
              ]
            TyIFix ()
_ Type TyName DefaultUni ()
pat Type TyName DefaultUni ()
arg ->
              (Type TyName DefaultUni () -> (Kind (), Type TyName DefaultUni ()))
-> [Type TyName DefaultUni ()]
-> [(Kind (), Type TyName DefaultUni ())]
forall a b. (a -> b) -> [a] -> [b]
map (() -> Kind ()
forall ann. ann -> Kind ann
Type (),) ([Type TyName DefaultUni ()]
 -> [(Kind (), Type TyName DefaultUni ())])
-> [Type TyName DefaultUni ()]
-> [(Kind (), Type TyName DefaultUni ())]
forall a b. (a -> b) -> a -> b
$
                [[Type TyName DefaultUni ()]] -> [Type TyName DefaultUni ()]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                  [
                    [ HasCallStack =>
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
fixKind TypeCtx
ctx Type TyName DefaultUni ()
pat (Kind () -> Type TyName DefaultUni ())
-> Kind () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
                    , HasCallStack =>
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
fixKind TypeCtx
ctx Type TyName DefaultUni ()
arg (Kind () -> Type TyName DefaultUni ())
-> Kind () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ () -> Kind ()
forall ann. ann -> Kind ann
Type ()
                    ]
                  , [ ()
-> 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
TyIFix () Type TyName DefaultUni ()
pat' (HasCallStack =>
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
fixKind TypeCtx
ctx Type TyName DefaultUni ()
arg Kind ()
kArg')
                    | (Kind ()
kPat', Type TyName DefaultUni ()
pat') <- HasCallStack =>
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
shrinkKindAndType TypeCtx
ctx (Kind () -> Kind ()
toPatFuncKind Kind ()
kArg, Type TyName DefaultUni ()
pat)
                    , Just Kind ()
kArg' <- [Kind () -> Maybe (Kind ())
fromPatFuncKind Kind ()
kPat']
                    ]
                  , [ ()
-> 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
TyIFix () (HasCallStack =>
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
TypeCtx
-> Type TyName DefaultUni ()
-> Kind ()
-> Type TyName DefaultUni ()
fixKind TypeCtx
ctx Type TyName DefaultUni ()
pat (Kind () -> Type TyName DefaultUni ())
-> Kind () -> Type TyName DefaultUni ()
forall a b. (a -> b) -> a -> b
$ Kind () -> Kind ()
toPatFuncKind Kind ()
kArg') Type TyName DefaultUni ()
arg'
                    | (Kind ()
kArg', Type TyName DefaultUni ()
arg') <- HasCallStack =>
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
shrinkKindAndType TypeCtx
ctx (Kind ()
kArg, Type TyName DefaultUni ()
arg)
                    ]
                  ]
              where
                kArg :: Kind ()
kArg = HasCallStack => TypeCtx -> Type TyName DefaultUni () -> Kind ()
TypeCtx -> Type TyName DefaultUni () -> Kind ()
unsafeInferKind TypeCtx
ctx Type TyName DefaultUni ()
arg
            TySOP ()
_ [[Type TyName DefaultUni ()]]
tyls ->
              (Type TyName DefaultUni () -> (Kind (), Type TyName DefaultUni ()))
-> [Type TyName DefaultUni ()]
-> [(Kind (), Type TyName DefaultUni ())]
forall a b. (a -> b) -> [a] -> [b]
map (() -> Kind ()
forall ann. ann -> Kind ann
Type (),) ([Type TyName DefaultUni ()]
 -> [(Kind (), Type TyName DefaultUni ())])
-> [Type TyName DefaultUni ()]
-> [(Kind (), Type TyName DefaultUni ())]
forall a b. (a -> b) -> a -> b
$
                [[Type TyName DefaultUni ()]] -> [Type TyName DefaultUni ()]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
                  [ -- Shrink to any type within the SOP.
                    [[Type TyName DefaultUni ()]] -> [Type TyName DefaultUni ()]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Type TyName DefaultUni ()]]
tyls
                  , -- Shrink either the entire sum or a product within it or a type within a product.
                    () -> [[Type TyName DefaultUni ()]] -> Type TyName DefaultUni ()
forall tyname (uni :: * -> *) ann.
ann -> [[Type tyname uni ann]] -> Type tyname uni ann
TySOP () ([[Type TyName DefaultUni ()]] -> Type TyName DefaultUni ())
-> [[[Type TyName DefaultUni ()]]] -> [Type TyName DefaultUni ()]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Type TyName DefaultUni ()] -> [[Type TyName DefaultUni ()]])
-> [[Type TyName DefaultUni ()]] -> [[[Type TyName DefaultUni ()]]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList ((Type TyName DefaultUni () -> [Type TyName DefaultUni ()])
-> [Type TyName DefaultUni ()] -> [[Type TyName DefaultUni ()]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList ((Type TyName DefaultUni () -> [Type TyName DefaultUni ()])
 -> [Type TyName DefaultUni ()] -> [[Type TyName DefaultUni ()]])
-> (Type TyName DefaultUni () -> [Type TyName DefaultUni ()])
-> [Type TyName DefaultUni ()]
-> [[Type TyName DefaultUni ()]]
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType TypeCtx
ctx) [[Type TyName DefaultUni ()]]
tyls
                  ]

-- | Shrink a type in a context assuming that it is of kind *.
shrinkType
  :: HasCallStack
  => TypeCtx
  -> Type TyName DefaultUni ()
  -> [Type TyName DefaultUni ()]
shrinkType :: HasCallStack =>
TypeCtx -> Type TyName DefaultUni () -> [Type TyName DefaultUni ()]
shrinkType TypeCtx
ctx Type TyName DefaultUni ()
ty = ((Kind (), Type TyName DefaultUni ()) -> Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
-> [Type TyName DefaultUni ()]
forall a b. (a -> b) -> [a] -> [b]
map (Kind (), Type TyName DefaultUni ()) -> Type TyName DefaultUni ()
forall a b. (a, b) -> b
snd ([(Kind (), Type TyName DefaultUni ())]
 -> [Type TyName DefaultUni ()])
-> [(Kind (), Type TyName DefaultUni ())]
-> [Type TyName DefaultUni ()]
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
TypeCtx
-> (Kind (), Type TyName DefaultUni ())
-> [(Kind (), Type TyName DefaultUni ())]
shrinkKindAndType TypeCtx
ctx (() -> Kind ()
forall ann. ann -> Kind ann
Type (), Type TyName DefaultUni ()
ty)

-- | Shrink a type of a given kind in a given context in a way that keeps its kind
shrinkTypeAtKind
  :: HasCallStack
  => TypeCtx
  -> Kind ()
  -> Type TyName DefaultUni ()
  -> [Type TyName DefaultUni ()]
-- It is unfortunate that we need to produce all those shrunk types just to filter out a lot of them
-- afterwards. But we still should get good coverage in the end.
shrinkTypeAtKind :: HasCallStack =>
TypeCtx
-> Kind ()
-> Type TyName DefaultUni ()
-> [Type TyName DefaultUni ()]
shrinkTypeAtKind TypeCtx
ctx Kind ()
k Type TyName DefaultUni ()
ty = [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
ctx (Kind ()
k, Type TyName DefaultUni ()
ty), Kind ()
k Kind () -> Kind () -> Bool
forall a. Eq a => a -> a -> Bool
== Kind ()
k']