{-|
Copyright   : (C) 2021, QBayLogic B.V.
License     : BSD2 (see the file LICENSE)
Maintainer  : QBayLogic B.V. <devops@qbaylogic.com>

Random kind-directed generation of Kind and Type.
-}

{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE LambdaCase #-}

module Clash.Hedgehog.Core.Type
  ( genKindFrom
  , genClosedKindFrom
  , genPolyTypeFrom
  , genClosedPolyType
  , genMonoTypeFrom
  , genClosedMonoType
  , genWithCodomain
  ) where

import Data.Coerce (coerce)
import Data.Monoid (Any(..))
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range

import Clash.Core.DataCon
import Clash.Core.HasType (piResultTys)
import Clash.Core.Pretty (showPpr)
import Clash.Core.Subst (aeqType)
import Clash.Core.TyCon
import Clash.Core.Type
import Clash.Core.TysPrim
import Clash.Unique

import Clash.Hedgehog.Core.Monad
import Clash.Hedgehog.Core.Name
import Clash.Hedgehog.Core.Var
import Clash.Hedgehog.Unique

-- | Classify a type or kind according to some criteria. The classification
-- of a type or kind is used to determine the pre-defined types / kinds which
-- can be used in hole fills. See 'classify' and 'useTyCon'.
--
data Class = Class
  { Class -> Any
cData :: !Any -- ^ Uses -XDataKinds
  , Class -> Any
cPoly :: !Any -- ^ Uses -XPolyKinds (if classifying a kind)
  , Class -> Any
cRankN :: !Any -- ^ Uses -XRankNTypes
  , Class -> Any
cFamily :: !Any -- ^ Uses -XTypeFamilies
  } deriving (Int -> Class -> ShowS
[Class] -> ShowS
Class -> String
(Int -> Class -> ShowS)
-> (Class -> String) -> ([Class] -> ShowS) -> Show Class
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Class] -> ShowS
$cshowList :: [Class] -> ShowS
show :: Class -> String
$cshow :: Class -> String
showsPrec :: Int -> Class -> ShowS
$cshowsPrec :: Int -> Class -> ShowS
Show)

instance Semigroup Class where
  Class
x <> :: Class -> Class -> Class
<> Class
y = Class :: Any -> Any -> Any -> Any -> Class
Class
    { cData :: Any
cData = Class -> Any
cData Class
x   Any -> Any -> Any
forall a. Semigroup a => a -> a -> a
<> Class -> Any
cData Class
y
    , cPoly :: Any
cPoly = Class -> Any
cPoly Class
x   Any -> Any -> Any
forall a. Semigroup a => a -> a -> a
<> Class -> Any
cPoly Class
y
    , cRankN :: Any
cRankN = Class -> Any
cRankN Class
x  Any -> Any -> Any
forall a. Semigroup a => a -> a -> a
<> Class -> Any
cRankN Class
y
    , cFamily :: Any
cFamily = Class -> Any
cFamily Class
x Any -> Any -> Any
forall a. Semigroup a => a -> a -> a
<> Class -> Any
cFamily Class
y
    }

instance Monoid Class where
  mempty :: Class
mempty = Any -> Any -> Any -> Any -> Class
Class Any
forall a. Monoid a => a
mempty Any
forall a. Monoid a => a
mempty Any
forall a. Monoid a => a
mempty Any
forall a. Monoid a => a
mempty

-- | Classify the groups that a type / kind belongs to, in order to filter out
-- kinds which are not compatible with the chosen 'CoreGenConfig'. This
-- combines multiple checks into one for efficiency, to prevent multiple passes
-- over each kind which can potentially be used.
--
classify :: Bool -> TyConMap -> KindOrType -> Class
classify :: Bool -> TyConMap -> KindOrType -> Class
classify Bool
isKind TyConMap
tcm = KindOrType -> Class
go
 where
  go :: KindOrType -> Class
go KindOrType
ty =
    case KindOrType -> TypeView
tyView KindOrType
ty of
      FunTy KindOrType
a KindOrType
b ->
        -- If the domain is polymorphic then we have -XRankNTypes.
        Class
forall a. Monoid a => a
mempty { cRankN :: Any
cRankN = Bool -> Any
Any (KindOrType -> Bool
isPolyTy KindOrType
a) } Class -> Class -> Class
forall a. Semigroup a => a -> a -> a
<> KindOrType -> Class
go KindOrType
a Class -> Class -> Class
forall a. Semigroup a => a -> a -> a
<> KindOrType -> Class
go KindOrType
b

      TyConApp TyConName
tcn [KindOrType]
args ->
        let tc :: TyCon
tc = TyConMap -> TyConName -> TyCon
forall a b. (HasCallStack, Uniquable a) => UniqMap b -> a -> b
lookupUniqMap' TyConMap
tcm TyConName
tcn
            isPoly :: Bool
isPoly = KindOrType -> Bool
isPolyTy (HasCallStack =>
TyConMap -> KindOrType -> [KindOrType] -> KindOrType
TyConMap -> KindOrType -> [KindOrType] -> KindOrType
piResultTys TyConMap
tcm (TyCon -> KindOrType
tyConKind TyCon
tc) [KindOrType]
args)
         in case TyConMap -> TyConName -> TyCon
forall a b. (HasCallStack, Uniquable a) => UniqMap b -> a -> b
lookupUniqMap' TyConMap
tcm TyConName
tcn of
              AlgTyCon{} ->
                -- If the constructor is algebraic then we have -XDataKinds if
                -- we are classifying a Kind instead of a Type.
                Class
forall a. Monoid a => a
mempty { cData :: Any
cData = Bool -> Any
Any Bool
isKind, cPoly :: Any
cPoly = Bool -> Any
Any Bool
isPoly }
                  Class -> Class -> Class
forall a. Semigroup a => a -> a -> a
<> [Class] -> Class
forall a. Monoid a => [a] -> a
mconcat ((KindOrType -> Class) -> [KindOrType] -> [Class]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap KindOrType -> Class
go [KindOrType]
args)

              PromotedDataCon{} ->
                -- If the constructor is a promoted data constructor then we
                -- have -XDataKinds.
                Class
forall a. Monoid a => a
mempty { cData :: Any
cData = Bool -> Any
Any Bool
True, cPoly :: Any
cPoly = Bool -> Any
Any Bool
isPoly }
                  Class -> Class -> Class
forall a. Semigroup a => a -> a -> a
<> [Class] -> Class
forall a. Monoid a => [a] -> a
mconcat ((KindOrType -> Class) -> [KindOrType] -> [Class]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap KindOrType -> Class
go [KindOrType]
args)

              FunTyCon{} ->
                -- If the constructor is a function then we have -XTypeFamilies.
                Class
forall a. Monoid a => a
mempty { cPoly :: Any
cPoly = Bool -> Any
Any Bool
isPoly, cFamily :: Any
cFamily = Bool -> Any
Any Bool
True }
                  Class -> Class -> Class
forall a. Semigroup a => a -> a -> a
<> [Class] -> Class
forall a. Monoid a => [a] -> a
mconcat ((KindOrType -> Class) -> [KindOrType] -> [Class]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap KindOrType -> Class
go [KindOrType]
args)

              PrimTyCon{}
                -- There's nothing special about Type.
                | KindOrType -> KindOrType -> Bool
aeqType KindOrType
ty KindOrType
liftedTypeKind -> Class
forall a. Monoid a => a
mempty

                -- If the constructor is Nat or Symbol, we have -XDataKinds.
                | KindOrType -> KindOrType -> Bool
aeqType KindOrType
ty KindOrType
typeNatKind -> Class
forall a. Monoid a => a
mempty { cData :: Any
cData = Bool -> Any
Any Bool
True }
                | KindOrType -> KindOrType -> Bool
aeqType KindOrType
ty KindOrType
typeSymbolKind -> Class
forall a. Monoid a => a
mempty { cData :: Any
cData = Bool -> Any
Any Bool
True }

                -- If the constructor is ~# then we have -XTypeFamilies.
                | KindOrType -> KindOrType -> Bool
aeqType KindOrType
ty KindOrType
eqPrimTy ->
                    Class
forall a. Monoid a => a
mempty { cPoly :: Any
cPoly = Bool -> Any
Any Bool
isPoly, cFamily :: Any
cFamily = Bool -> Any
Any Bool
True }
                      Class -> Class -> Class
forall a. Semigroup a => a -> a -> a
<> [Class] -> Class
forall a. Monoid a => [a] -> a
mconcat ((KindOrType -> Class) -> [KindOrType] -> [Class]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap KindOrType -> Class
go [KindOrType]
args)

                -- If the constructor is anything else we have -XDataKinds if
                -- we are classifying a Kind instead of a Type.
                | Bool
otherwise ->
                    Class
forall a. Monoid a => a
mempty { cData :: Any
cData = Bool -> Any
Any Bool
isKind, cPoly :: Any
cPoly = Bool -> Any
Any Bool
isPoly }
                      Class -> Class -> Class
forall a. Semigroup a => a -> a -> a
<> [Class] -> Class
forall a. Monoid a => [a] -> a
mconcat ((KindOrType -> Class) -> [KindOrType] -> [Class]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap KindOrType -> Class
go [KindOrType]
args)

      OtherType{} ->
        case KindOrType
ty of
          ForAllTy TyVar
_ KindOrType
a ->
            -- If there are quantifiers then we have polymorphism.
            Class
forall a. Monoid a => a
mempty { cPoly :: Any
cPoly = Bool -> Any
Any Bool
True } Class -> Class -> Class
forall a. Semigroup a => a -> a -> a
<> KindOrType -> Class
go KindOrType
a

          LitTy{} ->
            -- If there are literals then we have -XDataKinds.
            Class
forall a. Monoid a => a
mempty { cData :: Any
cData = Bool -> Any
Any Bool
True }

          VarTy TyVar
_ -> Class
forall a. Monoid a => a
mempty
          AppTy KindOrType
a KindOrType
b -> KindOrType -> Class
go KindOrType
a Class -> Class -> Class
forall a. Semigroup a => a -> a -> a
<> KindOrType -> Class
go KindOrType
b
          AnnType [Attr']
_ KindOrType
a -> KindOrType -> Class
go KindOrType
a
          ConstTy ConstTy
_ -> String -> Class
forall a. HasCallStack => String -> a
error (String
"classify: Naked ConstTy: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> KindOrType -> String
forall p. PrettyPrec p => p -> String
showPpr KindOrType
ty)

-- | Decide whether to use a type constructor based on the configuration and
-- the result of 'classifyKind'. A type constructor is not usable if it uses
-- any features which are not included in the current configuration.
--
useTyCon :: Bool -> CoreGenConfig -> TyConMap -> TyCon -> Bool
useTyCon :: Bool -> CoreGenConfig -> TyConMap -> TyCon -> Bool
useTyCon Bool
isKind CoreGenConfig
config TyConMap
tcm TyCon
tc
  | Bool
isKind
  = [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
and
      -- We don't generate equalities at the kind level, because the only
      -- witness we have for equality is a term-level primitive (_CO_).
      [ KindOrType -> Bool
isPrimKind KindOrType
ty
      , Any -> Bool
getAny (Class -> Any
cData Class
c) Bool -> Bool -> Bool
--> CoreGenConfig -> Bool
allowDataKinds CoreGenConfig
config
      , Any -> Bool
getAny (Class -> Any
cPoly Class
c) Bool -> Bool -> Bool
--> CoreGenConfig -> Bool
allowPolyKinds CoreGenConfig
config
      , Any -> Bool
getAny (Class -> Any
cRankN Class
c) Bool -> Bool -> Bool
--> CoreGenConfig -> Bool
allowRankNTypes CoreGenConfig
config
      , Any -> Bool
getAny (Class -> Any
cFamily Class
c) Bool -> Bool -> Bool
--> CoreGenConfig -> Bool
allowTypeFamilies CoreGenConfig
config
      ]

  | Bool
otherwise
  = [Bool] -> Bool
forall (t :: Type -> Type). Foldable t => t Bool -> Bool
and
      -- We don't generate Type, Nat or Symbol at the type level, because they
      -- have no term-level inhabitants. We also don't generate constraints
      -- like ~# because constraints are generated separately.
      [ Bool -> Bool
not (KindOrType -> Bool
isPrimKind KindOrType
ty)
      , Bool -> Bool
not (KindOrType -> KindOrType -> Bool
aeqType KindOrType
ty KindOrType
eqPrimTy)
      , Any -> Bool
getAny (Class -> Any
cData Class
c) Bool -> Bool -> Bool
--> CoreGenConfig -> Bool
allowDataKinds CoreGenConfig
config
      , Any -> Bool
getAny (Class -> Any
cRankN Class
c) Bool -> Bool -> Bool
--> CoreGenConfig -> Bool
allowRankNTypes CoreGenConfig
config
      , Any -> Bool
getAny (Class -> Any
cFamily Class
c) Bool -> Bool -> Bool
--> CoreGenConfig -> Bool
allowTypeFamilies CoreGenConfig
config
      ]
 where
  Bool
a --> :: Bool -> Bool -> Bool
--> Bool
b = Bool -> Bool
not Bool
a Bool -> Bool -> Bool
|| Bool
b
  isPrimKind :: KindOrType -> Bool
isPrimKind KindOrType
a = (KindOrType -> Bool) -> [KindOrType] -> Bool
forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
any (KindOrType -> KindOrType -> Bool
aeqType KindOrType
a) [KindOrType
liftedTypeKind, KindOrType
typeNatKind, KindOrType
typeSymbolKind]
  ty :: KindOrType
ty = TyConName -> KindOrType
mkTyConTy (TyCon -> TyConName
tyConName TyCon
tc)
  c :: Class
c = Bool -> TyConMap -> KindOrType -> Class
classify Bool
isKind TyConMap
tcm KindOrType
ty

-- | Generate a function where the codomain is the given type / kind. Any other
-- restrictions are enforced by the given generator. This can be used with
-- generators for kinds and types.
--
genWithCodomain
  :: forall m
   . (Alternative m, MonadGen m)
  => Kind
  -> CoreGenT m KindOrType
  -> CoreGenT m KindOrType
genWithCodomain :: KindOrType -> CoreGenT m KindOrType -> CoreGenT m KindOrType
genWithCodomain KindOrType
cod CoreGenT m KindOrType
gen = do
  ([Either TyVar KindOrType]
args, KindOrType
res) <- (KindOrType -> ([Either TyVar KindOrType], KindOrType))
-> CoreGenT m KindOrType
-> CoreGenT m ([Either TyVar KindOrType], KindOrType)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap KindOrType -> ([Either TyVar KindOrType], KindOrType)
splitFunForallTy CoreGenT m KindOrType
gen
  KindOrType -> CoreGenT m KindOrType
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (KindOrType -> [Either TyVar KindOrType] -> KindOrType
mkPolyFunTy KindOrType
cod ([Either TyVar KindOrType]
args [Either TyVar KindOrType]
-> [Either TyVar KindOrType] -> [Either TyVar KindOrType]
forall a. Semigroup a => a -> a -> a
<> [KindOrType -> Either TyVar KindOrType
forall a b. b -> Either a b
Right KindOrType
res]))

-- TODO
-- genConstraints
-- genConstrained

-- | Generate a closed kind (one without any free variables). If you want to
-- be able to use free variables in a kind, see 'genKindFrom'.
--
genClosedKindFrom
  :: forall m
   . (Alternative m, MonadGen m)
  => TyConMap
  -> Kind
  -> CoreGenT m Kind
genClosedKindFrom :: TyConMap -> KindOrType -> CoreGenT m KindOrType
genClosedKindFrom TyConMap
tcm =
  TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genKindFrom TyConMap
tcm UniqMap TyVar
forall a. UniqMap a
emptyUniqMap

-- | Generate a kind which is valid for the given 'TyConMap'. The kind may
-- contain free variables which are given in a 'UniqMap', and is a valid fit
-- for a hole with the given kind.
--
-- __N.B.__ Although the kind generated is a fit for the given hole, calling
-- a function like 'Clash.Core.HasType.inferCoreKindOf' may return a different
-- kind. This is because quantifiers are both the introduction rule for kind
-- arrows and a kind former of their own right, so for the hole
--
--   Type -> Type
--
-- a generated fit might be
--
--   forall a. a -> a
--
-- but this is then inferred to have the kind
--
--   Type
--
genKindFrom
  :: forall m
   . (Alternative m, MonadGen m)
  => TyConMap
  -> UniqMap TyVar
  -> Kind
  -> CoreGenT m Kind
genKindFrom :: TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genKindFrom TyConMap
tcm UniqMap TyVar
env KindOrType
hole =
  let genSub :: KindOrType -> CoreGenT m KindOrType
genSub = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genKindFrom TyConMap
tcm UniqMap TyVar
env
      -- A special case for holes of kind Type: we do not attempt to generate
      -- a fresh hole fit as this will produce an endless stream of (->) when
      -- not using -XPolyKinds.
      genOr :: CoreGenT m KindOrType
genOr = if KindOrType -> KindOrType -> Bool
aeqType KindOrType
hole KindOrType
liftedTypeKind
                then CoreGenT m KindOrType
forall (f :: Type -> Type) a. Alternative f => f a
empty
                else TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genFreshKind TyConMap
tcm UniqMap TyVar
env KindOrType
hole
   in [CoreGenT m KindOrType] -> CoreGenT m KindOrType
forall (m :: Type -> Type) a. MonadGen m => [m a] -> m a
Gen.choice
        [ Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyConOr Bool
True TyConMap
tcm KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub
            (UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyVarOr UniqMap TyVar
env KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub CoreGenT m KindOrType
genOr)
        , UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyVarOr UniqMap TyVar
env KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub
            (Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyConOr Bool
True TyConMap
tcm KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub CoreGenT m KindOrType
genOr)
        ]

-- | Generate a polymorphic type which is valid for the given environment.
-- The generated type should have the specified kind, and no free variables.
--
genClosedPolyType
  :: forall m
   . (Alternative m, MonadGen m)
  => TyConMap
  -> Kind
  -> CoreGenT m Type
genClosedPolyType :: TyConMap -> KindOrType -> CoreGenT m KindOrType
genClosedPolyType TyConMap
tcm =
  TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genPolyTypeFrom TyConMap
tcm UniqMap TyVar
forall a. UniqMap a
emptyUniqMap

-- | Generate a polymorphic type which is valid for the given environment.
-- The generated type should have the specified kind, and may contain the
-- specified free variables.
--
genPolyTypeFrom
  :: forall m
   . (Alternative m, MonadGen m)
  => TyConMap
  -> UniqMap TyVar
  -> Kind
  -> CoreGenT m Type
genPolyTypeFrom :: TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genPolyTypeFrom TyConMap
tcm UniqMap TyVar
env KindOrType
hole =
  let genSub :: KindOrType -> CoreGenT m KindOrType
genSub = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genPolyTypeFrom TyConMap
tcm UniqMap TyVar
env
      genOr :: CoreGenT m KindOrType
genOr  = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genFreshPolyType TyConMap
tcm UniqMap TyVar
env KindOrType
hole
   in [CoreGenT m KindOrType] -> CoreGenT m KindOrType
forall (m :: Type -> Type) a. MonadGen m => [m a] -> m a
Gen.choice
        [ Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyConOr Bool
False TyConMap
tcm KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub
            (UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyVarOr UniqMap TyVar
env KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub CoreGenT m KindOrType
genOr)
        , UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyVarOr UniqMap TyVar
env KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub
            (Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyConOr Bool
False TyConMap
tcm KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub CoreGenT m KindOrType
genOr)
        , TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genFreshPolyType TyConMap
tcm UniqMap TyVar
env KindOrType
hole
        ]

-- | Generate a monomorphic type which is valid for the given environment.
-- The generated type should have the specified kind, and no free variables.
--
genClosedMonoType
  :: forall m
   . (Alternative m, MonadGen m)
  => TyConMap
  -> Kind
  -> CoreGenT m Type
genClosedMonoType :: TyConMap -> KindOrType -> CoreGenT m KindOrType
genClosedMonoType TyConMap
tcm =
  TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genMonoTypeFrom TyConMap
tcm UniqMap TyVar
forall a. UniqMap a
emptyUniqMap

-- | Generate a monomorphic type which is valid for the given environment.
-- The generated type should have the specified kind, and may contain the
-- specified free variables.
--
genMonoTypeFrom
  :: forall m
   . (Alternative m, MonadGen m)
  => TyConMap
  -> UniqMap TyVar
  -> Kind
  -> CoreGenT m Type
genMonoTypeFrom :: TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genMonoTypeFrom TyConMap
tcm UniqMap TyVar
env KindOrType
hole =
  let genSub :: KindOrType -> CoreGenT m KindOrType
genSub = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genMonoTypeFrom TyConMap
tcm UniqMap TyVar
env
      -- TODO Maybe this can be changed for types, because it is always free
      -- to generate a forall, and the new binder may help break loops.
      genOr :: CoreGenT m KindOrType
genOr = if KindOrType -> KindOrType -> Bool
aeqType KindOrType
hole KindOrType
liftedTypeKind
                then CoreGenT m KindOrType
forall (f :: Type -> Type) a. Alternative f => f a
empty
                else TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genFreshMonoType TyConMap
tcm UniqMap TyVar
env KindOrType
hole
   in [CoreGenT m KindOrType] -> CoreGenT m KindOrType
forall (m :: Type -> Type) a. MonadGen m => [m a] -> m a
Gen.choice
        [ Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyConOr Bool
False TyConMap
tcm KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub
            (UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyVarOr UniqMap TyVar
env KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub CoreGenT m KindOrType
genOr)
        , UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyVarOr UniqMap TyVar
env KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub
            (Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyConOr Bool
False TyConMap
tcm KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub CoreGenT m KindOrType
genOr)
        , TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genFreshMonoType TyConMap
tcm UniqMap TyVar
env KindOrType
hole
        ]

-- | For the given hole, attempt to use a variable in the environment to fill
-- the hole, potentially solving subgoals if the variable is function kinded
-- and the hole is the codomain.
--
sampleTyVarOr
  :: forall m
   . (Alternative m, MonadGen m)
  => UniqMap TyVar
  -> Kind
  -> (Kind -> CoreGenT m KindOrType)
  -> CoreGenT m KindOrType
  -> CoreGenT m KindOrType
sampleTyVarOr :: UniqMap TyVar
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyVarOr UniqMap TyVar
env KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub CoreGenT m KindOrType
genOr =
  CoreGenT m KindOrType
sampleTyVar CoreGenT m KindOrType
-> CoreGenT m KindOrType -> CoreGenT m KindOrType
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> CoreGenT m KindOrType
genOr
 where
  sampleTyVar :: CoreGenT m KindOrType
sampleTyVar = do
    (TyVar
tv, [KindOrType]
holes) <- (TyVar -> Bool)
-> KindOrType -> UniqMap TyVar -> CoreGenT m (TyVar, [KindOrType])
forall (m :: Type -> Type) v.
(Alternative m, MonadGen m, HasType v) =>
(v -> Bool) -> KindOrType -> UniqMap v -> m (v, [KindOrType])
sampleUniqMap (Bool -> TyVar -> Bool
forall a b. a -> b -> a
const Bool
True) KindOrType
hole UniqMap TyVar
env
    [KindOrType]
holeFills <- (KindOrType -> CoreGenT m KindOrType)
-> [KindOrType] -> CoreGenT m [KindOrType]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse KindOrType -> CoreGenT m KindOrType
genSub [KindOrType]
holes

    KindOrType -> CoreGenT m KindOrType
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure ((KindOrType -> KindOrType -> KindOrType)
-> KindOrType -> [KindOrType] -> KindOrType
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr KindOrType -> KindOrType -> KindOrType
AppTy (TyVar -> KindOrType
VarTy TyVar
tv) [KindOrType]
holeFills)

-- | For the given hole, attempt to use a type constructor in the 'TyConMap' to
-- fill the hole, potentially solving subgoals if the constructor is function
-- kinded and the hole is the codomain.
--
sampleTyConOr
  :: forall m
   . (Alternative m, MonadGen m)
  => Bool
  -> TyConMap
  -> Kind
  -> (Kind -> CoreGenT m KindOrType)
  -> CoreGenT m KindOrType
  -> CoreGenT m KindOrType
sampleTyConOr :: Bool
-> TyConMap
-> KindOrType
-> (KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
-> CoreGenT m KindOrType
sampleTyConOr Bool
isKind TyConMap
tcm KindOrType
hole KindOrType -> CoreGenT m KindOrType
genSub CoreGenT m KindOrType
genOr =
  CoreGenT m KindOrType
sampleTyCon CoreGenT m KindOrType
-> CoreGenT m KindOrType -> CoreGenT m KindOrType
forall (f :: Type -> Type) a. Alternative f => f a -> f a -> f a
<|> CoreGenT m KindOrType
genOr
 where
  sampleTyCon :: CoreGenT m KindOrType
sampleTyCon = do
    CoreGenConfig
config <- CoreGenT m CoreGenConfig
forall r (m :: Type -> Type). MonadReader r m => m r
ask
    (TyCon
tc, [KindOrType]
holes) <- (TyCon -> Bool)
-> KindOrType -> TyConMap -> CoreGenT m (TyCon, [KindOrType])
forall (m :: Type -> Type) v.
(Alternative m, MonadGen m, HasType v, Bias v) =>
(v -> Bool) -> KindOrType -> UniqMap v -> m (v, [KindOrType])
sampleUniqMapBiased (Bool -> CoreGenConfig -> TyConMap -> TyCon -> Bool
useTyCon Bool
isKind CoreGenConfig
config TyConMap
tcm) KindOrType
hole TyConMap
tcm
    [KindOrType]
holeFills <- (KindOrType -> CoreGenT m KindOrType)
-> [KindOrType] -> CoreGenT m [KindOrType]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse KindOrType -> CoreGenT m KindOrType
genSub [KindOrType]
holes

    KindOrType -> CoreGenT m KindOrType
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TyConName -> [KindOrType] -> KindOrType
mkTyConApp (TyCon -> TyConName
tyConName TyCon
tc) [KindOrType]
holeFills)

genForAll
  :: forall m
   . (Alternative m, MonadGen m)
  => UniqMap TyVar
  -> Kind
  -> Kind
  -> (UniqMap TyVar -> Kind -> CoreGenT m KindOrType)
  -> CoreGenT m KindOrType
genForAll :: UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
genForAll UniqMap TyVar
env KindOrType
k1 KindOrType
k2 UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genSub = do
  TyVar
v <- KindOrType -> CoreGenT m TyName -> CoreGenT m TyVar
forall (m :: Type -> Type).
MonadGen m =>
KindOrType -> m TyName -> m TyVar
genTyVar KindOrType
k1 (UniqSet TyVar -> CoreGenT m TyName -> CoreGenT m TyName
forall (m :: Type -> Type) a b.
MonadGen m =>
UniqSet b -> m (Name a) -> m (Name a)
genFreshName (UniqMap TyVar -> UniqSet TyVar
forall a. UniqMap a -> UniqSet a
uniqMapToUniqSet UniqMap TyVar
env) CoreGenT m TyName
forall (m :: Type -> Type) a. MonadGen m => m (Name a)
genVarName)
  CoreGenT m KindOrType
-> (KindOrType -> KindOrType) -> CoreGenT m KindOrType
forall (m :: Type -> Type) a. MonadGen m => m a -> (a -> a) -> m a
Gen.subterm (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genSub (TyVar -> TyVar -> UniqMap TyVar -> UniqMap TyVar
forall a b. Uniquable a => a -> b -> UniqMap b -> UniqMap b
extendUniqMap TyVar
v TyVar
v UniqMap TyVar
env) KindOrType
k2) (TyVar -> KindOrType -> KindOrType
ForAllTy TyVar
v)

-- | Generate a "fresh" kind. This involves using the shape of the hole to
-- generate a layer of the result kind, then solving any subgoal with either
-- a variable, type constructor or another "fresh" kind.
--
genFreshKind
  :: forall m
   . (Alternative m, MonadGen m)
  => TyConMap
  -> UniqMap TyVar
  -> Kind
  -> CoreGenT m Kind
genFreshKind :: TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genFreshKind TyConMap
tcm UniqMap TyVar
env KindOrType
hole =
  CoreGenT m Bool
forall (m :: Type -> Type). Monad m => CoreGenT m Bool
canGenPolyKinds CoreGenT m Bool
-> (Bool -> CoreGenT m KindOrType) -> CoreGenT m KindOrType
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Bool
True -> TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genPolyKind TyConMap
tcm UniqMap TyVar
env KindOrType
hole
    Bool
False -> TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genMonoKind TyConMap
tcm UniqMap TyVar
env KindOrType
hole

-- | Generate a potentially polymorphic kind to fill a hole. This should not be
-- exported as it can be used to circumvent constraints on generation which are
-- given by the 'CoreGenConfig'.
--
genPolyKind
  :: forall m
   . (Alternative m, MonadGen m)
  => TyConMap
  -> UniqMap TyVar
  -> Kind
  -> CoreGenT m Kind
genPolyKind :: TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genPolyKind TyConMap
tcm UniqMap TyVar
env KindOrType
hole
  -- Hole: forall v. a
  | ForAllTy TyVar
v KindOrType
a <- KindOrType
hole
  = let env' :: UniqMap TyVar
env' = TyVar -> TyVar -> UniqMap TyVar -> UniqMap TyVar
forall a b. Uniquable a => a -> b -> UniqMap b -> UniqMap b
extendUniqMap TyVar
v TyVar
v UniqMap TyVar
env
     in CoreGenT m KindOrType
-> (KindOrType -> KindOrType) -> CoreGenT m KindOrType
forall (m :: Type -> Type) a. MonadGen m => m a -> (a -> a) -> m a
Gen.subterm (TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genKindFrom TyConMap
tcm UniqMap TyVar
env' KindOrType
a) (TyVar -> KindOrType -> KindOrType
ForAllTy TyVar
v)

  -- Hole: a -> b
  | FunTy KindOrType
a KindOrType
b <- KindOrType -> TypeView
tyView KindOrType
hole
  = UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
genForAll UniqMap TyVar
env KindOrType
a KindOrType
b (TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genKindFrom TyConMap
tcm)

  -- Hole: Type
  --
  -- If -XRankNTypes is not enabled, then we make sure the LHS of a generated
  -- arrow kind is a monomorphic kind.
  --
  -- As we shrink, it becomes more likely we just return Type for this hole.
  -- This rule is needed to prevent the generator recursing infinitely.
  | KindOrType -> KindOrType -> Bool
aeqType KindOrType
hole KindOrType
liftedTypeKind
  = CoreGenT m Bool
forall (m :: Type -> Type). Monad m => CoreGenT m Bool
canGenRankNTypes CoreGenT m Bool
-> (Bool -> CoreGenT m KindOrType) -> CoreGenT m KindOrType
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
True ->
        let polyGen :: CoreGenT m KindOrType
polyGen = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genKindFrom TyConMap
tcm UniqMap TyVar
env KindOrType
liftedTypeKind
         in [CoreGenT m KindOrType] -> CoreGenT m KindOrType
forall (m :: Type -> Type) a. MonadGen m => [m a] -> m a
Gen.choice
              [ CoreGenT m KindOrType
-> CoreGenT m KindOrType
-> (KindOrType -> KindOrType -> KindOrType)
-> CoreGenT m KindOrType
forall (m :: Type -> Type) a.
MonadGen m =>
m a -> m a -> (a -> a -> a) -> m a
Gen.subterm2 CoreGenT m KindOrType
polyGen CoreGenT m KindOrType
polyGen KindOrType -> KindOrType -> KindOrType
mkFunTy
              , UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
genForAll UniqMap TyVar
env KindOrType
liftedTypeKind KindOrType
liftedTypeKind (TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genKindFrom TyConMap
tcm)
              ]

      Bool
False ->
        let polyGen :: CoreGenT m KindOrType
polyGen = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genKindFrom TyConMap
tcm UniqMap TyVar
env KindOrType
liftedTypeKind
            monoGen :: CoreGenT m KindOrType
monoGen = (CoreGenConfig -> CoreGenConfig)
-> CoreGenT m KindOrType -> CoreGenT m KindOrType
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (\CoreGenConfig
r -> CoreGenConfig
r { allowPolyKinds :: Bool
allowPolyKinds = Bool
False }) CoreGenT m KindOrType
polyGen
         in [CoreGenT m KindOrType] -> CoreGenT m KindOrType
forall (m :: Type -> Type) a. MonadGen m => [m a] -> m a
Gen.choice
              [ CoreGenT m KindOrType
-> CoreGenT m KindOrType
-> (KindOrType -> KindOrType -> KindOrType)
-> CoreGenT m KindOrType
forall (m :: Type -> Type) a.
MonadGen m =>
m a -> m a -> (a -> a -> a) -> m a
Gen.subterm2 CoreGenT m KindOrType
monoGen CoreGenT m KindOrType
polyGen KindOrType -> KindOrType -> KindOrType
mkFunTy
              , UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
genForAll UniqMap TyVar
env KindOrType
liftedTypeKind KindOrType
liftedTypeKind (TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genKindFrom TyConMap
tcm)
              ]

  -- The hole is not anything which may result in a quantifier being generated,
  -- so we can fallback to genMonoKind for these cases.
  | Bool
otherwise
  = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genMonoKind TyConMap
tcm UniqMap TyVar
env KindOrType
hole

genMonoKind
  :: forall m
   . (Alternative m, MonadGen m)
  => TyConMap
  -> UniqMap TyVar
  -> Kind
  -> CoreGenT m Kind
genMonoKind :: TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genMonoKind TyConMap
tcm UniqMap TyVar
env KindOrType
hole
  -- Hole: C
  | ConstTy (TyCon TyConName
tcn) <- KindOrType
hole
  , Just TyCon
tc <- TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
lookupUniqMap TyConName
tcn TyConMap
tcm
  , let dcs :: [DataCon]
dcs = TyCon -> [DataCon]
tyConDataCons TyCon
tc
  , Bool -> Bool
not ([DataCon] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [DataCon]
dcs)
  = do DataCon
dc <- [DataCon] -> CoreGenT m DataCon
forall (m :: Type -> Type) a. MonadGen m => [a] -> m a
Gen.element [DataCon]
dcs
       [KindOrType]
args <- (KindOrType -> CoreGenT m KindOrType)
-> [KindOrType] -> CoreGenT m [KindOrType]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genKindFrom TyConMap
tcm UniqMap TyVar
env) (DataCon -> [KindOrType]
dcArgTys DataCon
dc)
       KindOrType -> CoreGenT m KindOrType
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TyConName -> [KindOrType] -> KindOrType
mkTyConApp (DcName -> TyConName
coerce (DataCon -> DcName
dcName DataCon
dc)) [KindOrType]
args)

  -- Hole: Nat
  | KindOrType -> KindOrType -> Bool
aeqType KindOrType
hole KindOrType
typeNatKind
  = CoreGenT m Bool
forall (m :: Type -> Type). Monad m => CoreGenT m Bool
canGenDataKinds CoreGenT m Bool
-> (Bool -> CoreGenT m KindOrType) -> CoreGenT m KindOrType
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
True -> LitTy -> KindOrType
LitTy (LitTy -> KindOrType) -> (Word -> LitTy) -> Word -> KindOrType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> LitTy
NumTy (Integer -> LitTy) -> (Word -> Integer) -> Word -> LitTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word -> Integer
forall a. Integral a => a -> Integer
toInteger (Word -> KindOrType) -> CoreGenT m Word -> CoreGenT m KindOrType
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Range Word -> CoreGenT m Word
forall (m :: Type -> Type). MonadGen m => Range Word -> m Word
Gen.word Range Word
forall a. (Bounded a, Integral a) => Range a
Range.linearBounded
      Bool
False -> String -> CoreGenT m KindOrType
forall a. HasCallStack => String -> a
error String
"genMonoKind: Cannot generate Nat without -XDataKinds"

  -- Hole: Symbol
  | KindOrType -> KindOrType -> Bool
aeqType KindOrType
hole KindOrType
typeSymbolKind
  = CoreGenT m Bool
forall (m :: Type -> Type). Monad m => CoreGenT m Bool
canGenDataKinds CoreGenT m Bool
-> (Bool -> CoreGenT m KindOrType) -> CoreGenT m KindOrType
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
True -> LitTy -> KindOrType
LitTy (LitTy -> KindOrType) -> (String -> LitTy) -> String -> KindOrType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> LitTy
SymTy (String -> KindOrType)
-> CoreGenT m String -> CoreGenT m KindOrType
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Range Int -> CoreGenT m Char -> CoreGenT m String
forall (m :: Type -> Type).
MonadGen m =>
Range Int -> m Char -> m String
Gen.string (Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
5 Int
10) CoreGenT m Char
forall (m :: Type -> Type). MonadGen m => m Char
Gen.alphaNum
      Bool
False -> String -> CoreGenT m KindOrType
forall a. HasCallStack => String -> a
error String
"genMonoKind: Cannot generate Symbol without -XDataKinds"

  -- Hole: Type
  --
  -- As we shrink, it becomes more likely we just return Type for this hole.
  -- This rule is needed to prevent the generator recursing infinitely.
  | KindOrType -> KindOrType -> Bool
aeqType KindOrType
hole KindOrType
liftedTypeKind
  = let gen :: CoreGenT m KindOrType
gen = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genKindFrom TyConMap
tcm UniqMap TyVar
env KindOrType
liftedTypeKind
     in CoreGenT m KindOrType
-> CoreGenT m KindOrType
-> (KindOrType -> KindOrType -> KindOrType)
-> CoreGenT m KindOrType
forall (m :: Type -> Type) a.
MonadGen m =>
m a -> m a -> (a -> a -> a) -> m a
Gen.subterm2 CoreGenT m KindOrType
gen CoreGenT m KindOrType
gen KindOrType -> KindOrType -> KindOrType
mkFunTy

  | Bool
otherwise
  = String -> CoreGenT m KindOrType
forall a. HasCallStack => String -> a
error (String
"genMonoKind: Cannot generate fit for hole: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> KindOrType -> String
forall p. PrettyPrec p => p -> String
showPpr KindOrType
hole)

genFreshPolyType
  :: forall m
   . (Alternative m, MonadGen m)
  => TyConMap
  -> UniqMap TyVar
  -> Kind
  -> CoreGenT m Type
genFreshPolyType :: TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genFreshPolyType TyConMap
tcm UniqMap TyVar
env KindOrType
hole
  | ForAllTy TyVar
tv KindOrType
kn <- KindOrType
hole
  = let env' :: UniqMap TyVar
env' = TyVar -> TyVar -> UniqMap TyVar -> UniqMap TyVar
forall a b. Uniquable a => a -> b -> UniqMap b -> UniqMap b
extendUniqMap TyVar
tv TyVar
tv UniqMap TyVar
env
     in CoreGenT m KindOrType
-> (KindOrType -> KindOrType) -> CoreGenT m KindOrType
forall (m :: Type -> Type) a. MonadGen m => m a -> (a -> a) -> m a
Gen.subterm (TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genPolyTypeFrom TyConMap
tcm UniqMap TyVar
env' KindOrType
kn) (TyVar -> KindOrType -> KindOrType
ForAllTy TyVar
tv)

  | FunTy KindOrType
a KindOrType
b <- KindOrType -> TypeView
tyView KindOrType
hole
  = UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
genForAll UniqMap TyVar
env KindOrType
a KindOrType
b (TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genPolyTypeFrom TyConMap
tcm)

  | KindOrType -> KindOrType -> Bool
aeqType KindOrType
hole KindOrType
liftedTypeKind
  = CoreGenT m Bool
forall (m :: Type -> Type). Monad m => CoreGenT m Bool
canGenRankNTypes CoreGenT m Bool
-> (Bool -> CoreGenT m KindOrType) -> CoreGenT m KindOrType
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
True ->
        let polyGen :: CoreGenT m KindOrType
polyGen = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genPolyTypeFrom TyConMap
tcm UniqMap TyVar
env KindOrType
liftedTypeKind
         in [CoreGenT m KindOrType] -> CoreGenT m KindOrType
forall (m :: Type -> Type) a. MonadGen m => [m a] -> m a
Gen.choice
              [ TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genFreshMonoType TyConMap
tcm UniqMap TyVar
env KindOrType
liftedTypeKind
              , CoreGenT m KindOrType
-> CoreGenT m KindOrType
-> (KindOrType -> KindOrType -> KindOrType)
-> CoreGenT m KindOrType
forall (m :: Type -> Type) a.
MonadGen m =>
m a -> m a -> (a -> a -> a) -> m a
Gen.subterm2 CoreGenT m KindOrType
polyGen CoreGenT m KindOrType
polyGen KindOrType -> KindOrType -> KindOrType
mkFunTy
              , UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
genForAll UniqMap TyVar
env KindOrType
liftedTypeKind KindOrType
liftedTypeKind (TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genPolyTypeFrom TyConMap
tcm)
              ]

      Bool
False ->
        let polyGen :: CoreGenT m KindOrType
polyGen = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genPolyTypeFrom TyConMap
tcm UniqMap TyVar
env KindOrType
liftedTypeKind
            monoGen :: CoreGenT m KindOrType
monoGen = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genMonoTypeFrom TyConMap
tcm UniqMap TyVar
env KindOrType
liftedTypeKind
         in [CoreGenT m KindOrType] -> CoreGenT m KindOrType
forall (m :: Type -> Type) a. MonadGen m => [m a] -> m a
Gen.choice
              [ TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genFreshMonoType TyConMap
tcm UniqMap TyVar
env KindOrType
hole
              , CoreGenT m KindOrType
-> CoreGenT m KindOrType
-> (KindOrType -> KindOrType -> KindOrType)
-> CoreGenT m KindOrType
forall (m :: Type -> Type) a.
MonadGen m =>
m a -> m a -> (a -> a -> a) -> m a
Gen.subterm2 CoreGenT m KindOrType
monoGen CoreGenT m KindOrType
polyGen KindOrType -> KindOrType -> KindOrType
mkFunTy
              , UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
UniqMap TyVar
-> KindOrType
-> KindOrType
-> (UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType)
-> CoreGenT m KindOrType
genForAll UniqMap TyVar
env KindOrType
liftedTypeKind KindOrType
liftedTypeKind (TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genPolyTypeFrom TyConMap
tcm)
              ]

  | Bool
otherwise
  = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genFreshMonoType TyConMap
tcm UniqMap TyVar
env KindOrType
hole

genFreshMonoType
  :: forall m
   . (Alternative m, MonadGen m)
  => TyConMap
  -> UniqMap TyVar
  -> Kind
  -> CoreGenT m Type
genFreshMonoType :: TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genFreshMonoType TyConMap
tcm UniqMap TyVar
env KindOrType
hole
  | ConstTy (TyCon TyConName
tcn) <- KindOrType
hole
  , Just TyCon
tc <- TyConName -> TyConMap -> Maybe TyCon
forall a b. Uniquable a => a -> UniqMap b -> Maybe b
lookupUniqMap TyConName
tcn TyConMap
tcm
  , let dcs :: [DataCon]
dcs = TyCon -> [DataCon]
tyConDataCons TyCon
tc
  , Bool -> Bool
not ([DataCon] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null [DataCon]
dcs)
  = do DataCon
dc <- [DataCon] -> CoreGenT m DataCon
forall (m :: Type -> Type) a. MonadGen m => [a] -> m a
Gen.element [DataCon]
dcs
       [KindOrType]
args <- (KindOrType -> CoreGenT m KindOrType)
-> [KindOrType] -> CoreGenT m [KindOrType]
forall (t :: Type -> Type) (f :: Type -> Type) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genMonoTypeFrom TyConMap
tcm UniqMap TyVar
env) (DataCon -> [KindOrType]
dcArgTys DataCon
dc)
       KindOrType -> CoreGenT m KindOrType
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (TyConName -> [KindOrType] -> KindOrType
mkTyConApp (DcName -> TyConName
coerce (DataCon -> DcName
dcName DataCon
dc)) [KindOrType]
args)

  | KindOrType -> KindOrType -> Bool
aeqType KindOrType
hole KindOrType
typeNatKind
  = CoreGenT m Bool
forall (m :: Type -> Type). Monad m => CoreGenT m Bool
canGenDataKinds CoreGenT m Bool
-> (Bool -> CoreGenT m KindOrType) -> CoreGenT m KindOrType
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
True -> LitTy -> KindOrType
LitTy (LitTy -> KindOrType) -> (Word -> LitTy) -> Word -> KindOrType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> LitTy
NumTy (Integer -> LitTy) -> (Word -> Integer) -> Word -> LitTy
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Word -> Integer
forall a. Integral a => a -> Integer
toInteger (Word -> KindOrType) -> CoreGenT m Word -> CoreGenT m KindOrType
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Range Word -> CoreGenT m Word
forall (m :: Type -> Type). MonadGen m => Range Word -> m Word
Gen.word Range Word
forall a. (Bounded a, Integral a) => Range a
Range.linearBounded
      Bool
False -> String -> CoreGenT m KindOrType
forall a. HasCallStack => String -> a
error String
"genFreshMonoType: Cannot generate Nat without -XDataKinds"

  | KindOrType -> KindOrType -> Bool
aeqType KindOrType
hole KindOrType
typeSymbolKind
  = CoreGenT m Bool
forall (m :: Type -> Type). Monad m => CoreGenT m Bool
canGenDataKinds CoreGenT m Bool
-> (Bool -> CoreGenT m KindOrType) -> CoreGenT m KindOrType
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
      Bool
True -> LitTy -> KindOrType
LitTy (LitTy -> KindOrType) -> (String -> LitTy) -> String -> KindOrType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> LitTy
SymTy (String -> KindOrType)
-> CoreGenT m String -> CoreGenT m KindOrType
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Range Int -> CoreGenT m Char -> CoreGenT m String
forall (m :: Type -> Type).
MonadGen m =>
Range Int -> m Char -> m String
Gen.string (Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
5 Int
10) CoreGenT m Char
forall (m :: Type -> Type). MonadGen m => m Char
Gen.alphaNum
      Bool
False -> String -> CoreGenT m KindOrType
forall a. HasCallStack => String -> a
error String
"genFreshMonoType: Cannot generate Symbol without -XDataKinds"

  | KindOrType -> KindOrType -> Bool
aeqType KindOrType
hole KindOrType
liftedTypeKind
  = let gen :: CoreGenT m KindOrType
gen = TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
forall (m :: Type -> Type).
(Alternative m, MonadGen m) =>
TyConMap -> UniqMap TyVar -> KindOrType -> CoreGenT m KindOrType
genMonoTypeFrom TyConMap
tcm UniqMap TyVar
env KindOrType
liftedTypeKind
     in CoreGenT m KindOrType
-> CoreGenT m KindOrType
-> (KindOrType -> KindOrType -> KindOrType)
-> CoreGenT m KindOrType
forall (m :: Type -> Type) a.
MonadGen m =>
m a -> m a -> (a -> a -> a) -> m a
Gen.subterm2 CoreGenT m KindOrType
gen CoreGenT m KindOrType
gen KindOrType -> KindOrType -> KindOrType
mkFunTy

  | Bool
otherwise
  = String -> CoreGenT m KindOrType
forall a. HasCallStack => String -> a
error (String
"genFreshMonoType: Cannot generate fit for hole: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> KindOrType -> String
forall p. PrettyPrec p => p -> String
showPpr KindOrType
hole)