-- | Nominal (named) types declaration, instantiation, construction, and access.

{-# LANGUAGE FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts, TemplateHaskell, EmptyCase #-}

module Hyper.Type.AST.Nominal
    ( NominalDecl(..), nParams, nScheme, W_NominalDecl(..)
    , NominalInst(..), nId, nArgs
    , ToNom(..), tnId, tnVal, W_ToNom(..)
    , FromNom(..), _FromNom

    , HasNominalInst(..)
    , NomVarTypes
    , MonadNominals(..)
    , LoadedNominalDecl, loadNominalDecl
    ) where

import           Control.Applicative (Alternative(..))
import           Control.Lens (Prism')
import qualified Control.Lens as Lens
import           Control.Monad.Trans.Writer (execWriterT)
import           Generics.Constraints (Constraints)
import           Hyper
import           Hyper.Class.Context (HContext(..))
import           Hyper.Class.Optic
import           Hyper.Class.Traversable (ContainedH(..))
import           Hyper.Class.ZipMatch (ZipMatch(..))
import           Hyper.Infer
import           Hyper.Recurse
import           Hyper.Type.AST.FuncType (FuncType(..))
import           Hyper.Type.AST.Map (TermMap(..), _TermMap)
import           Hyper.Type.AST.Scheme
import           Hyper.Unify
import           Hyper.Unify.Generalize (GTerm(..), _GMono, instantiateWith, instantiateForAll)
import           Hyper.Unify.New (newTerm)
import           Hyper.Unify.QuantifiedVar (HasQuantifiedVar(..), OrdQVar)
import           Hyper.Unify.Term (UTerm(..))
import qualified Text.PrettyPrint as P
import           Text.PrettyPrint.HughesPJClass (Pretty(..), maybeParens)

import           Hyper.Internal.Prelude

type family NomVarTypes (t :: HyperType) :: HyperType

-- | A declaration of a nominal type.
data NominalDecl typ h = NominalDecl
    { NominalDecl typ h -> NomVarTypes typ # QVars
_nParams :: NomVarTypes typ # QVars
    , NominalDecl typ h -> Scheme (NomVarTypes typ) typ h
_nScheme :: Scheme (NomVarTypes typ) typ h
    } deriving (forall x. NominalDecl typ h -> Rep (NominalDecl typ h) x)
-> (forall x. Rep (NominalDecl typ h) x -> NominalDecl typ h)
-> Generic (NominalDecl typ h)
forall x. Rep (NominalDecl typ h) x -> NominalDecl typ h
forall x. NominalDecl typ h -> Rep (NominalDecl typ h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (typ :: HyperType) (h :: AHyperType) x.
Rep (NominalDecl typ h) x -> NominalDecl typ h
forall (typ :: HyperType) (h :: AHyperType) x.
NominalDecl typ h -> Rep (NominalDecl typ h) x
$cto :: forall (typ :: HyperType) (h :: AHyperType) x.
Rep (NominalDecl typ h) x -> NominalDecl typ h
$cfrom :: forall (typ :: HyperType) (h :: AHyperType) x.
NominalDecl typ h -> Rep (NominalDecl typ h) x
Generic

-- | An instantiation of a nominal type
data NominalInst nomId varTypes h = NominalInst
    { NominalInst nomId varTypes h -> nomId
_nId :: nomId
    , NominalInst nomId varTypes h
-> varTypes # QVarInstances (GetHyperType h)
_nArgs :: varTypes # QVarInstances (GetHyperType h)
    } deriving (forall x.
 NominalInst nomId varTypes h
 -> Rep (NominalInst nomId varTypes h) x)
-> (forall x.
    Rep (NominalInst nomId varTypes h) x
    -> NominalInst nomId varTypes h)
-> Generic (NominalInst nomId varTypes h)
forall x.
Rep (NominalInst nomId varTypes h) x
-> NominalInst nomId varTypes h
forall x.
NominalInst nomId varTypes h
-> Rep (NominalInst nomId varTypes h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall nomId (varTypes :: HyperType) (h :: AHyperType) x.
Rep (NominalInst nomId varTypes h) x
-> NominalInst nomId varTypes h
forall nomId (varTypes :: HyperType) (h :: AHyperType) x.
NominalInst nomId varTypes h
-> Rep (NominalInst nomId varTypes h) x
$cto :: forall nomId (varTypes :: HyperType) (h :: AHyperType) x.
Rep (NominalInst nomId varTypes h) x
-> NominalInst nomId varTypes h
$cfrom :: forall nomId (varTypes :: HyperType) (h :: AHyperType) x.
NominalInst nomId varTypes h
-> Rep (NominalInst nomId varTypes h) x
Generic

-- | Nominal data constructor.
--
-- Wrap content with a data constructor
-- (analogues to a data constructor of a Haskell `newtype`'s).
--
-- Introduces the nominal's foralled type variables into the value's scope.
data ToNom nomId term h = ToNom
    { ToNom nomId term h -> nomId
_tnId :: nomId
    , ToNom nomId term h -> h :# term
_tnVal :: h :# term
    } deriving (forall x. ToNom nomId term h -> Rep (ToNom nomId term h) x)
-> (forall x. Rep (ToNom nomId term h) x -> ToNom nomId term h)
-> Generic (ToNom nomId term h)
forall x. Rep (ToNom nomId term h) x -> ToNom nomId term h
forall x. ToNom nomId term h -> Rep (ToNom nomId term h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall nomId (term :: HyperType) (h :: AHyperType) x.
Rep (ToNom nomId term h) x -> ToNom nomId term h
forall nomId (term :: HyperType) (h :: AHyperType) x.
ToNom nomId term h -> Rep (ToNom nomId term h) x
$cto :: forall nomId (term :: HyperType) (h :: AHyperType) x.
Rep (ToNom nomId term h) x -> ToNom nomId term h
$cfrom :: forall nomId (term :: HyperType) (h :: AHyperType) x.
ToNom nomId term h -> Rep (ToNom nomId term h) x
Generic

-- | Access the data in a nominally typed value.
--
-- Analogues to a getter of a Haskell `newtype`.
newtype FromNom nomId (term :: HyperType) (h :: AHyperType) = FromNom nomId
    deriving newtype (FromNom nomId term h -> FromNom nomId term h -> Bool
(FromNom nomId term h -> FromNom nomId term h -> Bool)
-> (FromNom nomId term h -> FromNom nomId term h -> Bool)
-> Eq (FromNom nomId term h)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall nomId (term :: HyperType) (h :: AHyperType).
Eq nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
/= :: FromNom nomId term h -> FromNom nomId term h -> Bool
$c/= :: forall nomId (term :: HyperType) (h :: AHyperType).
Eq nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
== :: FromNom nomId term h -> FromNom nomId term h -> Bool
$c== :: forall nomId (term :: HyperType) (h :: AHyperType).
Eq nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
Eq, Eq (FromNom nomId term h)
Eq (FromNom nomId term h)
-> (FromNom nomId term h -> FromNom nomId term h -> Ordering)
-> (FromNom nomId term h -> FromNom nomId term h -> Bool)
-> (FromNom nomId term h -> FromNom nomId term h -> Bool)
-> (FromNom nomId term h -> FromNom nomId term h -> Bool)
-> (FromNom nomId term h -> FromNom nomId term h -> Bool)
-> (FromNom nomId term h
    -> FromNom nomId term h -> FromNom nomId term h)
-> (FromNom nomId term h
    -> FromNom nomId term h -> FromNom nomId term h)
-> Ord (FromNom nomId term h)
FromNom nomId term h -> FromNom nomId term h -> Bool
FromNom nomId term h -> FromNom nomId term h -> Ordering
FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
Eq (FromNom nomId term h)
forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Ordering
forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h
min :: FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h
$cmin :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h
max :: FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h
$cmax :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h
-> FromNom nomId term h -> FromNom nomId term h
>= :: FromNom nomId term h -> FromNom nomId term h -> Bool
$c>= :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
> :: FromNom nomId term h -> FromNom nomId term h -> Bool
$c> :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
<= :: FromNom nomId term h -> FromNom nomId term h -> Bool
$c<= :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
< :: FromNom nomId term h -> FromNom nomId term h -> Bool
$c< :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Bool
compare :: FromNom nomId term h -> FromNom nomId term h -> Ordering
$ccompare :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
FromNom nomId term h -> FromNom nomId term h -> Ordering
$cp1Ord :: forall nomId (term :: HyperType) (h :: AHyperType).
Ord nomId =>
Eq (FromNom nomId term h)
Ord, Get (FromNom nomId term h)
[FromNom nomId term h] -> Put
FromNom nomId term h -> Put
(FromNom nomId term h -> Put)
-> Get (FromNom nomId term h)
-> ([FromNom nomId term h] -> Put)
-> Binary (FromNom nomId term h)
forall t. (t -> Put) -> Get t -> ([t] -> Put) -> Binary t
forall nomId (term :: HyperType) (h :: AHyperType).
Binary nomId =>
Get (FromNom nomId term h)
forall nomId (term :: HyperType) (h :: AHyperType).
Binary nomId =>
[FromNom nomId term h] -> Put
forall nomId (term :: HyperType) (h :: AHyperType).
Binary nomId =>
FromNom nomId term h -> Put
putList :: [FromNom nomId term h] -> Put
$cputList :: forall nomId (term :: HyperType) (h :: AHyperType).
Binary nomId =>
[FromNom nomId term h] -> Put
get :: Get (FromNom nomId term h)
$cget :: forall nomId (term :: HyperType) (h :: AHyperType).
Binary nomId =>
Get (FromNom nomId term h)
put :: FromNom nomId term h -> Put
$cput :: forall nomId (term :: HyperType) (h :: AHyperType).
Binary nomId =>
FromNom nomId term h -> Put
Binary, FromNom nomId term h -> ()
(FromNom nomId term h -> ()) -> NFData (FromNom nomId term h)
forall a. (a -> ()) -> NFData a
forall nomId (term :: HyperType) (h :: AHyperType).
NFData nomId =>
FromNom nomId term h -> ()
rnf :: FromNom nomId term h -> ()
$crnf :: forall nomId (term :: HyperType) (h :: AHyperType).
NFData nomId =>
FromNom nomId term h -> ()
NFData)
    deriving stock (Int -> FromNom nomId term h -> ShowS
[FromNom nomId term h] -> ShowS
FromNom nomId term h -> String
(Int -> FromNom nomId term h -> ShowS)
-> (FromNom nomId term h -> String)
-> ([FromNom nomId term h] -> ShowS)
-> Show (FromNom nomId term h)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall nomId (term :: HyperType) (h :: AHyperType).
Show nomId =>
Int -> FromNom nomId term h -> ShowS
forall nomId (term :: HyperType) (h :: AHyperType).
Show nomId =>
[FromNom nomId term h] -> ShowS
forall nomId (term :: HyperType) (h :: AHyperType).
Show nomId =>
FromNom nomId term h -> String
showList :: [FromNom nomId term h] -> ShowS
$cshowList :: forall nomId (term :: HyperType) (h :: AHyperType).
Show nomId =>
[FromNom nomId term h] -> ShowS
show :: FromNom nomId term h -> String
$cshow :: forall nomId (term :: HyperType) (h :: AHyperType).
Show nomId =>
FromNom nomId term h -> String
showsPrec :: Int -> FromNom nomId term h -> ShowS
$cshowsPrec :: forall nomId (term :: HyperType) (h :: AHyperType).
Show nomId =>
Int -> FromNom nomId term h -> ShowS
Show, (forall x. FromNom nomId term h -> Rep (FromNom nomId term h) x)
-> (forall x. Rep (FromNom nomId term h) x -> FromNom nomId term h)
-> Generic (FromNom nomId term h)
forall x. Rep (FromNom nomId term h) x -> FromNom nomId term h
forall x. FromNom nomId term h -> Rep (FromNom nomId term h) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall nomId (term :: HyperType) (h :: AHyperType) x.
Rep (FromNom nomId term h) x -> FromNom nomId term h
forall nomId (term :: HyperType) (h :: AHyperType) x.
FromNom nomId term h -> Rep (FromNom nomId term h) x
$cto :: forall nomId (term :: HyperType) (h :: AHyperType) x.
Rep (FromNom nomId term h) x -> FromNom nomId term h
$cfrom :: forall nomId (term :: HyperType) (h :: AHyperType) x.
FromNom nomId term h -> Rep (FromNom nomId term h) x
Generic)

-- | A nominal declaration loaded into scope in an inference monad.
data LoadedNominalDecl typ v = LoadedNominalDecl
    { LoadedNominalDecl typ v
-> NomVarTypes typ # QVarInstances (GetHyperType v)
_lnParams :: NomVarTypes typ # QVarInstances (GetHyperType v)
    , LoadedNominalDecl typ v
-> NomVarTypes typ # QVarInstances (GetHyperType v)
_lnForalls :: NomVarTypes typ # QVarInstances (GetHyperType v)
    , LoadedNominalDecl typ v -> GTerm (GetHyperType v) # typ
_lnType :: GTerm (GetHyperType v) # typ
    } deriving (forall x.
 LoadedNominalDecl typ v -> Rep (LoadedNominalDecl typ v) x)
-> (forall x.
    Rep (LoadedNominalDecl typ v) x -> LoadedNominalDecl typ v)
-> Generic (LoadedNominalDecl typ v)
forall x.
Rep (LoadedNominalDecl typ v) x -> LoadedNominalDecl typ v
forall x.
LoadedNominalDecl typ v -> Rep (LoadedNominalDecl typ v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (typ :: HyperType) (v :: AHyperType) x.
Rep (LoadedNominalDecl typ v) x -> LoadedNominalDecl typ v
forall (typ :: HyperType) (v :: AHyperType) x.
LoadedNominalDecl typ v -> Rep (LoadedNominalDecl typ v) x
$cto :: forall (typ :: HyperType) (v :: AHyperType) x.
Rep (LoadedNominalDecl typ v) x -> LoadedNominalDecl typ v
$cfrom :: forall (typ :: HyperType) (v :: AHyperType) x.
LoadedNominalDecl typ v -> Rep (LoadedNominalDecl typ v) x
Generic

makeLenses ''NominalDecl
makeLenses ''NominalInst
makeLenses ''ToNom
makePrisms ''FromNom
makeCommonInstances [''NominalDecl, ''NominalInst, ''ToNom, ''LoadedNominalDecl]
makeHTraversableAndBases ''NominalDecl
makeHTraversableApplyAndBases ''ToNom
makeHTraversableApplyAndBases ''FromNom
makeHMorph ''ToNom
makeZipMatch ''ToNom
makeZipMatch ''FromNom
makeHContext ''ToNom
makeHContext ''FromNom

instance HNodes v => HNodes (NominalInst n v) where
    type HNodesConstraint (NominalInst n v) c = HNodesConstraint v c
    type HWitnessType (NominalInst n v) = HWitnessType v
    {-# INLINE hLiftConstraint #-}
    hLiftConstraint :: HWitness (NominalInst n v) n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitness HWitnessType (NominalInst n v) n
w) = HWitness v n -> Proxy c -> (c n => r) -> r
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint @v (HWitnessType v n -> HWitness v n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType v n
HWitnessType (NominalInst n v) n
w)

instance HFunctor v => HFunctor (NominalInst n v) where
    {-# INLINE hmap #-}
    hmap :: (forall (n :: HyperType).
 HWitness (NominalInst n v) n -> (p # n) -> q # n)
-> (NominalInst n v # p) -> NominalInst n v # q
hmap forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> q # n
f = (v ('AHyperType (QVarInstances p))
 -> Identity (v ('AHyperType (QVarInstances q))))
-> (NominalInst n v # p) -> Identity (NominalInst n v # q)
forall nomId (varTypes :: HyperType) (h :: AHyperType)
       (varTypes :: HyperType) (h :: AHyperType).
Lens
  (NominalInst nomId varTypes h)
  (NominalInst nomId varTypes h)
  (varTypes # QVarInstances (GetHyperType h))
  (varTypes # QVarInstances (GetHyperType h))
nArgs ((v ('AHyperType (QVarInstances p))
  -> Identity (v ('AHyperType (QVarInstances q))))
 -> (NominalInst n v # p) -> Identity (NominalInst n v # q))
-> (v ('AHyperType (QVarInstances p))
    -> v ('AHyperType (QVarInstances q)))
-> (NominalInst n v # p)
-> NominalInst n v # q
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (n :: HyperType).
 HWitness v n -> (QVarInstances p # n) -> QVarInstances q # n)
-> v ('AHyperType (QVarInstances p))
-> v ('AHyperType (QVarInstances q))
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (\(HWitness HWitnessType v n
w) -> (Map (QVar n) (p ('AHyperType n))
 -> Identity (Map (QVar n) (q # n)))
-> (QVarInstances p # n) -> Identity (QVarInstances q # n)
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
       (typ :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar n) (p ('AHyperType n))
  -> Identity (Map (QVar n) (q # n)))
 -> (QVarInstances p # n) -> Identity (QVarInstances q # n))
-> ((p ('AHyperType n) -> Identity (q # n))
    -> Map (QVar n) (p ('AHyperType n))
    -> Identity (Map (QVar n) (q # n)))
-> (p ('AHyperType n) -> Identity (q # n))
-> (QVarInstances p # n)
-> Identity (QVarInstances q # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p ('AHyperType n) -> Identity (q # n))
-> Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (q # n))
forall (f :: * -> *) a b. Functor f => Setter (f a) (f b) a b
Lens.mapped ((p ('AHyperType n) -> Identity (q # n))
 -> (QVarInstances p # n) -> Identity (QVarInstances q # n))
-> (p ('AHyperType n) -> q # n)
-> (QVarInstances p # n)
-> QVarInstances q # n
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ HWitness (NominalInst n v) n -> p ('AHyperType n) -> q # n
forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> q # n
f (HWitnessType (NominalInst n v) n -> HWitness (NominalInst n v) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType v n
HWitnessType (NominalInst n v) n
w))

instance HFoldable v => HFoldable (NominalInst n v) where
    {-# INLINE hfoldMap #-}
    hfoldMap :: (forall (n :: HyperType).
 HWitness (NominalInst n v) n -> (p # n) -> a)
-> (NominalInst n v # p) -> a
hfoldMap forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> a
f =
        (forall (n :: HyperType).
 HWitness v n -> (QVarInstances p # n) -> a)
-> (v # QVarInstances p) -> a
forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (\(HWitness HWitnessType v n
w) -> ((p # n) -> a) -> Map (QVar n) (p # n) -> a
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (HWitness (NominalInst n v) n -> (p # n) -> a
forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> a
f (HWitnessType (NominalInst n v) n -> HWitness (NominalInst n v) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType v n
HWitnessType (NominalInst n v) n
w)) (Map (QVar n) (p # n) -> a)
-> ((QVarInstances p # n) -> Map (QVar n) (p # n))
-> (QVarInstances p # n)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QVarInstances p # n)
-> Getting
     (Map (QVar n) (p # n)) (QVarInstances p # n) (Map (QVar n) (p # n))
-> Map (QVar n) (p # n)
forall s a. s -> Getting a s a -> a
^. Getting
  (Map (QVar n) (p # n)) (QVarInstances p # n) (Map (QVar n) (p # n))
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
       (typ :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances)) ((v # QVarInstances p) -> a)
-> ((NominalInst n v # p) -> v # QVarInstances p)
-> (NominalInst n v # p)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((NominalInst n v # p)
-> Getting
     (v # QVarInstances p) (NominalInst n v # p) (v # QVarInstances p)
-> v # QVarInstances p
forall s a. s -> Getting a s a -> a
^. Getting
  (v # QVarInstances p) (NominalInst n v # p) (v # QVarInstances p)
forall nomId (varTypes :: HyperType) (h :: AHyperType)
       (varTypes :: HyperType) (h :: AHyperType).
Lens
  (NominalInst nomId varTypes h)
  (NominalInst nomId varTypes h)
  (varTypes # QVarInstances (GetHyperType h))
  (varTypes # QVarInstances (GetHyperType h))
nArgs)

instance HTraversable v => HTraversable (NominalInst n v) where
    {-# INLINE hsequence #-}
    hsequence :: (NominalInst n v # ContainedH f p) -> f (NominalInst n v # p)
hsequence (NominalInst n
n v # QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
v) =
        (forall (n :: HyperType).
 HWitness v n
 -> (QVarInstances (ContainedH f p) # n) -> f (QVarInstances p # n))
-> (v # QVarInstances (ContainedH f p)) -> f (v # QVarInstances p)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse ((QVarInstances (ContainedH f p) ('AHyperType n)
 -> f (QVarInstances p ('AHyperType n)))
-> HWitness v n
-> QVarInstances (ContainedH f p) ('AHyperType n)
-> f (QVarInstances p ('AHyperType n))
forall a b. a -> b -> a
const ((Map
   (QVar (GetHyperType ('AHyperType n)))
   (ContainedH f p ('AHyperType n))
 -> f (Map
         (QVar (GetHyperType ('AHyperType n))) (p ('AHyperType n))))
-> QVarInstances (ContainedH f p) ('AHyperType n)
-> f (QVarInstances p ('AHyperType n))
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
       (typ :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((ContainedH f p ('AHyperType n) -> f (p ('AHyperType n)))
-> Map (QVar n) (ContainedH f p ('AHyperType n))
-> f (Map (QVar n) (p ('AHyperType n)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse ContainedH f p ('AHyperType n) -> f (p ('AHyperType n))
forall (f :: * -> *) (p :: HyperType) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH))) v # QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
v # QVarInstances (ContainedH f p)
v
        f (v # QVarInstances p)
-> ((v # QVarInstances p) -> NominalInst n v # p)
-> f (NominalInst n v # p)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> n
-> (v # QVarInstances (GetHyperType ('AHyperType p)))
-> NominalInst n v # p
forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst n
n

instance
    ( Eq nomId
    , ZipMatch varTypes
    , HTraversable varTypes
    , HNodesConstraint varTypes ZipMatch
    , HNodesConstraint varTypes OrdQVar
    ) =>
    ZipMatch (NominalInst nomId varTypes) where

    {-# INLINE zipMatch #-}
    zipMatch :: (NominalInst nomId varTypes # p)
-> (NominalInst nomId varTypes # q)
-> Maybe (NominalInst nomId varTypes # (p :*: q))
zipMatch (NominalInst nomId
xId varTypes # QVarInstances (GetHyperType ('AHyperType p))
x) (NominalInst nomId
yId varTypes # QVarInstances (GetHyperType ('AHyperType q))
y)
        | nomId
xId nomId -> nomId -> Bool
forall a. Eq a => a -> a -> Bool
/= nomId
yId = Maybe (NominalInst nomId varTypes # (p :*: q))
forall a. Maybe a
Nothing
        | Bool
otherwise =
            (varTypes # QVarInstances p)
-> (varTypes # QVarInstances q)
-> Maybe (varTypes # (QVarInstances p :*: QVarInstances q))
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
ZipMatch h =>
(h # p) -> (h # q) -> Maybe (h # (p :*: q))
zipMatch varTypes # QVarInstances p
varTypes # QVarInstances (GetHyperType ('AHyperType p))
x varTypes # QVarInstances q
varTypes # QVarInstances (GetHyperType ('AHyperType q))
y
            Maybe (varTypes # (QVarInstances p :*: QVarInstances q))
-> ((varTypes # (QVarInstances p :*: QVarInstances q))
    -> Maybe (varTypes # QVarInstances (p :*: q)))
-> Maybe (varTypes # QVarInstances (p :*: q))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall (n :: HyperType).
 HWitness varTypes n
 -> ((QVarInstances p :*: QVarInstances q) # n)
 -> Maybe (QVarInstances (p :*: q) # n))
-> (varTypes # (QVarInstances p :*: QVarInstances q))
-> Maybe (varTypes # QVarInstances (p :*: q))
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse
                ( Proxy ZipMatch
forall k (t :: k). Proxy t
Proxy @ZipMatch Proxy ZipMatch
-> (ZipMatch n =>
    HWitness varTypes n
    -> ((QVarInstances p :*: QVarInstances q) # n)
    -> Maybe (QVarInstances (p :*: q) # n))
-> HWitness varTypes n
-> ((QVarInstances p :*: QVarInstances q) # n)
-> Maybe (QVarInstances (p :*: q) # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*# Proxy OrdQVar
forall k (t :: k). Proxy t
Proxy @OrdQVar Proxy OrdQVar
-> (OrdQVar n =>
    ((QVarInstances p :*: QVarInstances q) # n)
    -> Maybe (QVarInstances (p :*: q) # n))
-> HWitness varTypes n
-> ((QVarInstances p :*: QVarInstances q) # n)
-> Maybe (QVarInstances (p :*: q) # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
                    \(QVarInstances Map (QVar (GetHyperType ('AHyperType n))) (p ('AHyperType n))
c0 :*: QVarInstances Map (QVar (GetHyperType ('AHyperType n))) (q ('AHyperType n))
c1) ->
                    (TermMap (QVar n) n # p)
-> (TermMap (QVar n) n # q)
-> Maybe (TermMap (QVar n) n # (p :*: q))
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
ZipMatch h =>
(h # p) -> (h # q) -> Maybe (h # (p :*: q))
zipMatch (Map (QVar n) ('AHyperType p :# n) -> TermMap (QVar n) n # p
forall h2 (expr2 :: HyperType) (f2 :: AHyperType).
Map h2 (f2 :# expr2) -> TermMap h2 expr2 f2
TermMap Map (QVar n) ('AHyperType p :# n)
Map (QVar (GetHyperType ('AHyperType n))) (p ('AHyperType n))
c0) (Map (QVar n) ('AHyperType q :# n) -> TermMap (QVar n) n # q
forall h2 (expr2 :: HyperType) (f2 :: AHyperType).
Map h2 (f2 :# expr2) -> TermMap h2 expr2 f2
TermMap Map (QVar n) ('AHyperType q :# n)
Map (QVar (GetHyperType ('AHyperType n))) (q ('AHyperType n))
c1)
                    Maybe (TermMap (QVar n) n # (p :*: q))
-> ((TermMap (QVar n) n # (p :*: q))
    -> Map (QVar n) ((p :*: q) # n))
-> Maybe (Map (QVar n) ((p :*: q) # n))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> ((TermMap (QVar n) n # (p :*: q))
-> Getting
     (Map (QVar n) ((p :*: q) # n))
     (TermMap (QVar n) n # (p :*: q))
     (Map (QVar n) ((p :*: q) # n))
-> Map (QVar n) ((p :*: q) # n)
forall s a. s -> Getting a s a -> a
^. Getting
  (Map (QVar n) ((p :*: q) # n))
  (TermMap (QVar n) n # (p :*: q))
  (Map (QVar n) ((p :*: q) # n))
forall h1 (expr1 :: HyperType) (f1 :: AHyperType) h2
       (expr2 :: HyperType) (f2 :: AHyperType).
Iso
  (TermMap h1 expr1 f1)
  (TermMap h2 expr2 f2)
  (Map h1 (f1 :# expr1))
  (Map h2 (f2 :# expr2))
_TermMap)
                    Maybe (Map (QVar n) ((p :*: q) # n))
-> (Map (QVar n) ((p :*: q) # n) -> QVarInstances (p :*: q) # n)
-> Maybe (QVarInstances (p :*: q) # n)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Map (QVar n) ((p :*: q) # n) -> QVarInstances (p :*: q) # n
forall (h :: HyperType) (typ :: AHyperType).
Map (QVar (GetHyperType typ)) (h typ) -> QVarInstances h typ
QVarInstances
                )
            Maybe (varTypes # QVarInstances (p :*: q))
-> ((varTypes # QVarInstances (p :*: q))
    -> NominalInst nomId varTypes # (p :*: q))
-> Maybe (NominalInst nomId varTypes # (p :*: q))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> nomId
-> (varTypes
    # QVarInstances (GetHyperType ('AHyperType (p :*: q))))
-> NominalInst nomId varTypes # (p :*: q)
forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
xId

instance
    ( HFunctor varTypes
    , HContext varTypes
    , HNodesConstraint varTypes OrdQVar
    ) => HContext (NominalInst nomId varTypes) where
    hcontext :: (NominalInst nomId varTypes # p)
-> NominalInst nomId varTypes
   # (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
hcontext (NominalInst nomId
n varTypes # QVarInstances (GetHyperType ('AHyperType p))
args) =
        (varTypes # QVarInstances p)
-> varTypes
   # (HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
      :*: QVarInstances p)
forall (h :: HyperType) (p :: HyperType).
HContext h =>
(h # p) -> h # (HFunc p (Const (h # p)) :*: p)
hcontext varTypes # QVarInstances p
varTypes # QVarInstances (GetHyperType ('AHyperType p))
args
        (varTypes
 # (HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
    :*: QVarInstances p))
-> ((varTypes
     # (HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
        :*: QVarInstances p))
    -> varTypes
       # QVarInstances
           (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p))
-> varTypes
   # QVarInstances
       (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
forall a b. a -> (a -> b) -> b
& (forall (n :: HyperType).
 HWitness varTypes n
 -> ((HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
      :*: QVarInstances p)
     # n)
 -> QVarInstances
      (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
    # n)
-> (varTypes
    # (HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
       :*: QVarInstances p))
-> varTypes
   # QVarInstances
       (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
            ( Proxy OrdQVar
forall k (t :: k). Proxy t
Proxy @OrdQVar Proxy OrdQVar
-> (OrdQVar n =>
    ((HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
      :*: QVarInstances p)
     # n)
    -> QVarInstances
         (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
       # n)
-> HWitness varTypes n
-> ((HFunc (QVarInstances p) (Const (varTypes # QVarInstances p))
     :*: QVarInstances p)
    # n)
-> QVarInstances
     (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
   # n
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
                \(HFunc QVarInstances p ('AHyperType n)
-> Const (varTypes # QVarInstances p) ('AHyperType n)
c :*: QVarInstances p ('AHyperType n)
x) ->
                QVarInstances p ('AHyperType n)
x QVarInstances p ('AHyperType n)
-> (QVarInstances p ('AHyperType n)
    -> QVarInstances
         (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
       # n)
-> QVarInstances
     (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
   # n
forall a b. a -> (a -> b) -> b
& (Map (QVar n) (p ('AHyperType n))
 -> Identity
      (Map
         (QVar n)
         ((:*:)
            (HFunc p (Const (NominalInst nomId varTypes # p)))
            p
            ('AHyperType n))))
-> QVarInstances p ('AHyperType n)
-> Identity
     (QVarInstances
        (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
      # n)
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
       (typ :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar n) (p ('AHyperType n))
  -> Identity
       (Map
          (QVar n)
          ((:*:)
             (HFunc p (Const (NominalInst nomId varTypes # p)))
             p
             ('AHyperType n))))
 -> QVarInstances p ('AHyperType n)
 -> Identity
      (QVarInstances
         (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
       # n))
-> (Indexed
      (QVar n)
      (p ('AHyperType n))
      (Identity
         ((:*:)
            (HFunc p (Const (NominalInst nomId varTypes # p)))
            p
            ('AHyperType n)))
    -> Map (QVar n) (p ('AHyperType n))
    -> Identity
         (Map
            (QVar n)
            ((:*:)
               (HFunc p (Const (NominalInst nomId varTypes # p)))
               p
               ('AHyperType n))))
-> Indexed
     (QVar n)
     (p ('AHyperType n))
     (Identity
        ((:*:)
           (HFunc p (Const (NominalInst nomId varTypes # p)))
           p
           ('AHyperType n)))
-> QVarInstances p ('AHyperType n)
-> Identity
     (QVarInstances
        (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
      # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Indexed
  (QVar n)
  (p ('AHyperType n))
  (Identity
     ((:*:)
        (HFunc p (Const (NominalInst nomId varTypes # p)))
        p
        ('AHyperType n)))
-> Map (QVar n) (p ('AHyperType n))
-> Identity
     (Map
        (QVar n)
        ((:*:)
           (HFunc p (Const (NominalInst nomId varTypes # p)))
           p
           ('AHyperType n)))
forall i (f :: * -> *) a b.
FunctorWithIndex i f =>
IndexedSetter i (f a) (f b) a b
Lens.imapped (Indexed
   (QVar n)
   (p ('AHyperType n))
   (Identity
      ((:*:)
         (HFunc p (Const (NominalInst nomId varTypes # p)))
         p
         ('AHyperType n)))
 -> QVarInstances p ('AHyperType n)
 -> Identity
      (QVarInstances
         (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
       # n))
-> (QVar n
    -> p ('AHyperType n)
    -> (:*:)
         (HFunc p (Const (NominalInst nomId varTypes # p)))
         p
         ('AHyperType n))
-> QVarInstances p ('AHyperType n)
-> QVarInstances
     (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
   # n
forall i s t a b.
AnIndexedSetter i s t a b -> (i -> a -> b) -> s -> t
%@~
                \QVar n
k p ('AHyperType n)
v ->
                (p ('AHyperType n)
 -> Const (NominalInst nomId varTypes # p) ('AHyperType n))
-> HFunc p (Const (NominalInst nomId varTypes # p)) ('AHyperType n)
forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc
                ( \p ('AHyperType n)
newV ->
                    QVarInstances p ('AHyperType n)
x
                    QVarInstances p ('AHyperType n)
-> (QVarInstances p ('AHyperType n)
    -> QVarInstances p ('AHyperType n))
-> QVarInstances p ('AHyperType n)
forall a b. a -> (a -> b) -> b
& (Map (QVar n) (p ('AHyperType n))
 -> Identity (Map (QVar n) (p ('AHyperType n))))
-> QVarInstances p ('AHyperType n)
-> Identity (QVarInstances p ('AHyperType n))
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
       (typ :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar n) (p ('AHyperType n))
  -> Identity (Map (QVar n) (p ('AHyperType n))))
 -> QVarInstances p ('AHyperType n)
 -> Identity (QVarInstances p ('AHyperType n)))
-> ((Maybe (p ('AHyperType n))
     -> Identity (Maybe (p ('AHyperType n))))
    -> Map (QVar n) (p ('AHyperType n))
    -> Identity (Map (QVar n) (p ('AHyperType n))))
-> (Maybe (p ('AHyperType n))
    -> Identity (Maybe (p ('AHyperType n))))
-> QVarInstances p ('AHyperType n)
-> Identity (QVarInstances p ('AHyperType n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map (QVar n) (p ('AHyperType n)))
-> Lens'
     (Map (QVar n) (p ('AHyperType n)))
     (Maybe (IxValue (Map (QVar n) (p ('AHyperType n)))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
Lens.at Index (Map (QVar n) (p ('AHyperType n)))
QVar n
k ((Maybe (p ('AHyperType n))
  -> Identity (Maybe (p ('AHyperType n))))
 -> QVarInstances p ('AHyperType n)
 -> Identity (QVarInstances p ('AHyperType n)))
-> p ('AHyperType n)
-> QVarInstances p ('AHyperType n)
-> QVarInstances p ('AHyperType n)
forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ p ('AHyperType n)
newV
                    QVarInstances p ('AHyperType n)
-> (QVarInstances p ('AHyperType n)
    -> Const (varTypes # QVarInstances p) ('AHyperType n))
-> Const (varTypes # QVarInstances p) ('AHyperType n)
forall a b. a -> (a -> b) -> b
& QVarInstances p ('AHyperType n)
-> Const (varTypes # QVarInstances p) ('AHyperType n)
c Const (varTypes # QVarInstances p) ('AHyperType n)
-> (Const (varTypes # QVarInstances p) ('AHyperType n)
    -> varTypes # QVarInstances p)
-> varTypes # QVarInstances p
forall a b. a -> (a -> b) -> b
& Const (varTypes # QVarInstances p) ('AHyperType n)
-> varTypes # QVarInstances p
forall a k (b :: k). Const a b -> a
getConst (varTypes # QVarInstances p)
-> ((varTypes # QVarInstances p) -> NominalInst nomId varTypes # p)
-> NominalInst nomId varTypes # p
forall a b. a -> (a -> b) -> b
& nomId
-> (varTypes # QVarInstances (GetHyperType ('AHyperType p)))
-> NominalInst nomId varTypes # p
forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
n
                    (NominalInst nomId varTypes # p)
-> ((NominalInst nomId varTypes # p)
    -> Const (NominalInst nomId varTypes # p) ('AHyperType n))
-> Const (NominalInst nomId varTypes # p) ('AHyperType n)
forall a b. a -> (a -> b) -> b
& (NominalInst nomId varTypes # p)
-> Const (NominalInst nomId varTypes # p) ('AHyperType n)
forall k a (b :: k). a -> Const a b
Const
                ) HFunc p (Const (NominalInst nomId varTypes # p)) ('AHyperType n)
-> p ('AHyperType n)
-> (:*:)
     (HFunc p (Const (NominalInst nomId varTypes # p)))
     p
     ('AHyperType n)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: p ('AHyperType n)
v
            )
        (varTypes
 # QVarInstances
     (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p))
-> ((varTypes
     # QVarInstances
         (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p))
    -> NominalInst nomId varTypes
       # (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p))
-> NominalInst nomId varTypes
   # (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
forall a b. a -> (a -> b) -> b
& nomId
-> (varTypes
    # QVarInstances
        (GetHyperType
           ('AHyperType
              (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p))))
-> NominalInst nomId varTypes
   # (HFunc p (Const (NominalInst nomId varTypes # p)) :*: p)
forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
n

instance Constraints (ToNom nomId term h) Pretty => Pretty (ToNom nomId term h) where
    pPrintPrec :: PrettyLevel -> Rational -> ToNom nomId term h -> Doc
pPrintPrec PrettyLevel
lvl Rational
p (ToNom nomId
nomId h :# term
term) =
        (nomId -> Doc
forall a. Pretty a => a -> Doc
pPrint nomId
nomId Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
P.text String
"#") Doc -> Doc -> Doc
P.<+> PrettyLevel -> Rational -> (h :# term) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
11 h :# term
term
        Doc -> (Doc -> Doc) -> Doc
forall a b. a -> (a -> b) -> b
& Bool -> Doc -> Doc
maybeParens (Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
10)

class    (Pretty (QVar h), Pretty (outer :# h)) => PrettyConstraints outer h
instance (Pretty (QVar h), Pretty (outer :# h)) => PrettyConstraints outer h

instance
    ( Pretty nomId
    , HApply varTypes, HFoldable varTypes
    , HNodesConstraint varTypes (PrettyConstraints h)
    ) =>
    Pretty (NominalInst nomId varTypes h) where

    pPrint :: NominalInst nomId varTypes h -> Doc
pPrint (NominalInst nomId
n varTypes # QVarInstances (GetHyperType h)
vars) =
        nomId -> Doc
forall a. Pretty a => a -> Doc
pPrint nomId
n Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
        [Doc] -> Doc
joinArgs
        ((forall (n :: HyperType).
 HWitness varTypes n
 -> (QVarInstances (GetHyperType h) # n) -> [Doc])
-> (varTypes # QVarInstances (GetHyperType h)) -> [Doc]
forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (Proxy (PrettyConstraints h)
forall k (t :: k). Proxy t
Proxy @(PrettyConstraints h) Proxy (PrettyConstraints h)
-> (PrettyConstraints h n =>
    (QVarInstances (GetHyperType h) # n) -> [Doc])
-> HWitness varTypes n
-> (QVarInstances (GetHyperType h) # n)
-> [Doc]
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> PrettyConstraints h n =>
(QVarInstances (GetHyperType h) # n) -> [Doc]
forall (typ :: AHyperType) (h :: HyperType).
(Pretty (QVar (GetHyperType typ)), Pretty (h typ)) =>
QVarInstances h typ -> [Doc]
mkArgs) varTypes # QVarInstances (GetHyperType h)
vars)
        where
            joinArgs :: [Doc] -> Doc
joinArgs [] = Doc
forall a. Monoid a => a
mempty
            joinArgs [Doc]
xs = String -> Doc
P.text String
"[" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
P.sep (Doc -> [Doc] -> [Doc]
P.punctuate (String -> Doc
P.text String
",") [Doc]
xs) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
P.text String
"]"
            mkArgs :: QVarInstances h typ -> [Doc]
mkArgs (QVarInstances Map (QVar (GetHyperType typ)) (h typ)
m) =
                Map (QVar (GetHyperType typ)) (h typ)
m Map (QVar (GetHyperType typ)) (h typ)
-> IndexedGetting
     (QVar (GetHyperType typ))
     (Endo [(QVar (GetHyperType typ), h typ)])
     (Map (QVar (GetHyperType typ)) (h typ))
     (h typ)
-> [(QVar (GetHyperType typ), h typ)]
forall s i a. s -> IndexedGetting i (Endo [(i, a)]) s a -> [(i, a)]
^@.. IndexedGetting
  (QVar (GetHyperType typ))
  (Endo [(QVar (GetHyperType typ), h typ)])
  (Map (QVar (GetHyperType typ)) (h typ))
  (h typ)
forall i (t :: * -> *) a b.
TraversableWithIndex i t =>
IndexedTraversal i (t a) (t b) a b
Lens.itraversed [(QVar (GetHyperType typ), h typ)]
-> ((QVar (GetHyperType typ), h typ) -> Doc) -> [Doc]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
                \(QVar (GetHyperType typ)
h, h typ
v) ->
                (QVar (GetHyperType typ) -> Doc
forall a. Pretty a => a -> Doc
pPrint QVar (GetHyperType typ)
h Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
P.text String
":") Doc -> Doc -> Doc
P.<+> h typ -> Doc
forall a. Pretty a => a -> Doc
pPrint h typ
v

{-# ANN module "HLint: ignore Use camelCase" #-}
data W_LoadedNominalDecl t n where
    E_LoadedNominalDecl_Body :: HRecWitness t n -> W_LoadedNominalDecl t n
    E_LoadedNominalDecl_NomVarTypes :: HWitness (NomVarTypes t) n -> W_LoadedNominalDecl t n

instance (RNodes t, HNodes (NomVarTypes t)) => HNodes (LoadedNominalDecl t) where
    type HNodesConstraint (LoadedNominalDecl t) c =
        ( HNodesConstraint (NomVarTypes t) c
        , c t
        , Recursive c
        )
    type HWitnessType (LoadedNominalDecl t) = W_LoadedNominalDecl t
    {-# INLINE hLiftConstraint #-}
    hLiftConstraint :: HWitness (LoadedNominalDecl t) n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitness (E_LoadedNominalDecl_Body w)) = HWitness (HFlip GTerm t) n -> Proxy c -> (c n => r) -> r
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint @(HFlip GTerm _) (HWitnessType (HFlip GTerm t) n -> HWitness (HFlip GTerm t) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType (HFlip GTerm t) n
HRecWitness t n
w)
    hLiftConstraint (HWitness (E_LoadedNominalDecl_NomVarTypes w)) = HWitness (NomVarTypes t) n -> Proxy c -> (c n => r) -> r
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint HWitness (NomVarTypes t) n
w

instance
    (Recursively HFunctor typ, HFunctor (NomVarTypes typ)) =>
    HFunctor (LoadedNominalDecl typ) where
    {-# INLINE hmap #-}
    hmap :: (forall (n :: HyperType).
 HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n)
-> (LoadedNominalDecl typ # p) -> LoadedNominalDecl typ # q
hmap forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n
f (LoadedNominalDecl NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mp NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mf GTerm (GetHyperType ('AHyperType p)) # typ
t) =
        (NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType q)))
-> (NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType q)))
-> (GTerm (GetHyperType ('AHyperType q)) # typ)
-> LoadedNominalDecl typ # q
forall (typ :: HyperType) (v :: AHyperType).
(NomVarTypes typ # QVarInstances (GetHyperType v))
-> (NomVarTypes typ # QVarInstances (GetHyperType v))
-> (GTerm (GetHyperType v) # typ)
-> LoadedNominalDecl typ v
LoadedNominalDecl ((NomVarTypes typ # QVarInstances p)
-> NomVarTypes typ # QVarInstances q
onMap NomVarTypes typ # QVarInstances p
NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mp) ((NomVarTypes typ # QVarInstances p)
-> NomVarTypes typ # QVarInstances q
onMap NomVarTypes typ # QVarInstances p
NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mf)
        (GTerm p ('AHyperType typ)
GTerm (GetHyperType ('AHyperType p)) # typ
t GTerm p ('AHyperType typ)
-> (GTerm p ('AHyperType typ) -> GTerm q # typ) -> GTerm q # typ
forall a b. a -> (a -> b) -> b
& ((HFlip GTerm typ # p) -> Identity (HFlip GTerm typ # q))
-> GTerm p ('AHyperType typ) -> Identity (GTerm q # typ)
forall (f0 :: HyperType -> HyperType) (k0 :: HyperType)
       (x0 :: HyperType) (f1 :: HyperType -> HyperType) (k1 :: HyperType)
       (x1 :: HyperType).
Iso (f0 k0 # x0) (f1 k1 # x1) (HFlip f0 x0 # k0) (HFlip f1 x1 # k1)
hflipped (((HFlip GTerm typ # p) -> Identity (HFlip GTerm typ # q))
 -> GTerm p ('AHyperType typ) -> Identity (GTerm q # typ))
-> ((HFlip GTerm typ # p) -> HFlip GTerm typ # q)
-> GTerm p ('AHyperType typ)
-> GTerm q # typ
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (n :: HyperType).
 HWitness (HFlip GTerm typ) n -> (p # n) -> q # n)
-> (HFlip GTerm typ # p) -> HFlip GTerm typ # q
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (\(HWitness HWitnessType (HFlip GTerm typ) n
w) -> HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n
forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n
f (HWitnessType (LoadedNominalDecl typ) n
-> HWitness (LoadedNominalDecl typ) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (HRecWitness typ n -> W_LoadedNominalDecl typ n
forall (t :: HyperType) (n :: HyperType).
HRecWitness t n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_Body HWitnessType (HFlip GTerm typ) n
HRecWitness typ n
w))))
        where
            onMap :: (NomVarTypes typ # QVarInstances p)
-> NomVarTypes typ # QVarInstances q
onMap = (forall (n :: HyperType).
 HWitness (NomVarTypes typ) n
 -> (QVarInstances p # n) -> QVarInstances q # n)
-> (NomVarTypes typ # QVarInstances p)
-> NomVarTypes typ # QVarInstances q
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (\HWitness (NomVarTypes typ) n
w -> (Map (QVar n) (p ('AHyperType n))
 -> Identity (Map (QVar n) (q # n)))
-> (QVarInstances p # n) -> Identity (QVarInstances q # n)
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
       (typ :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar n) (p ('AHyperType n))
  -> Identity (Map (QVar n) (q # n)))
 -> (QVarInstances p # n) -> Identity (QVarInstances q # n))
-> ((p ('AHyperType n) -> Identity (q # n))
    -> Map (QVar n) (p ('AHyperType n))
    -> Identity (Map (QVar n) (q # n)))
-> (p ('AHyperType n) -> Identity (q # n))
-> (QVarInstances p # n)
-> Identity (QVarInstances q # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p ('AHyperType n) -> Identity (q # n))
-> Map (QVar n) (p ('AHyperType n))
-> Identity (Map (QVar n) (q # n))
forall (f :: * -> *) a b. Functor f => Setter (f a) (f b) a b
Lens.mapped ((p ('AHyperType n) -> Identity (q # n))
 -> (QVarInstances p # n) -> Identity (QVarInstances q # n))
-> (p ('AHyperType n) -> q # n)
-> (QVarInstances p # n)
-> QVarInstances q # n
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ HWitness (LoadedNominalDecl typ) n -> p ('AHyperType n) -> q # n
forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n
f (HWitnessType (LoadedNominalDecl typ) n
-> HWitness (LoadedNominalDecl typ) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (HWitness (NomVarTypes typ) n -> W_LoadedNominalDecl typ n
forall (t :: HyperType) (n :: HyperType).
HWitness (NomVarTypes t) n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_NomVarTypes HWitness (NomVarTypes typ) n
w)))

instance
    (Recursively HFoldable typ, HFoldable (NomVarTypes typ)) =>
    HFoldable (LoadedNominalDecl typ) where
    {-# INLINE hfoldMap #-}
    hfoldMap :: (forall (n :: HyperType).
 HWitness (LoadedNominalDecl typ) n -> (p # n) -> a)
-> (LoadedNominalDecl typ # p) -> a
hfoldMap forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
f (LoadedNominalDecl NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mp NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mf GTerm (GetHyperType ('AHyperType p)) # typ
t) =
        (NomVarTypes typ # QVarInstances p) -> a
onMap NomVarTypes typ # QVarInstances p
NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mp a -> a -> a
forall a. Semigroup a => a -> a -> a
<> (NomVarTypes typ # QVarInstances p) -> a
onMap NomVarTypes typ # QVarInstances p
NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mf a -> a -> a
forall a. Semigroup a => a -> a -> a
<>
        (forall (n :: HyperType).
 HWitness (HFlip GTerm typ) n -> (p # n) -> a)
-> (HFlip GTerm typ # p) -> a
forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (\(HWitness HWitnessType (HFlip GTerm typ) n
w) -> HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
f (HWitnessType (LoadedNominalDecl typ) n
-> HWitness (LoadedNominalDecl typ) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (HRecWitness typ n -> W_LoadedNominalDecl typ n
forall (t :: HyperType) (n :: HyperType).
HRecWitness t n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_Body HWitnessType (HFlip GTerm typ) n
HRecWitness typ n
w))) (Tagged (GTerm p # typ) (Identity (GTerm p # typ))
-> Tagged (HFlip GTerm typ # p) (Identity (HFlip GTerm typ # p))
forall (f0 :: HyperType -> HyperType) (x0 :: HyperType)
       (k0 :: HyperType) (f1 :: HyperType -> HyperType) (x1 :: HyperType)
       (k1 :: HyperType).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip (Tagged (GTerm p # typ) (Identity (GTerm p # typ))
 -> Tagged (HFlip GTerm typ # p) (Identity (HFlip GTerm typ # p)))
-> (GTerm p # typ) -> HFlip GTerm typ # p
forall t b. AReview t b -> b -> t
# GTerm p # typ
GTerm (GetHyperType ('AHyperType p)) # typ
t)
        where
            onMap :: (NomVarTypes typ # QVarInstances p) -> a
onMap =
                (forall (n :: HyperType).
 HWitness (NomVarTypes typ) n -> (QVarInstances p # n) -> a)
-> (NomVarTypes typ # QVarInstances p) -> a
forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (\HWitness (NomVarTypes typ) n
w -> ((p # n) -> a) -> Map (QVar n) (p # n) -> a
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
f (HWitnessType (LoadedNominalDecl typ) n
-> HWitness (LoadedNominalDecl typ) n
forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (HWitness (NomVarTypes typ) n -> W_LoadedNominalDecl typ n
forall (t :: HyperType) (n :: HyperType).
HWitness (NomVarTypes t) n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_NomVarTypes HWitness (NomVarTypes typ) n
w)))
                (Map (QVar n) (p # n) -> a)
-> ((QVarInstances p # n) -> Map (QVar n) (p # n))
-> (QVarInstances p # n)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QVarInstances p # n)
-> Getting
     (Map (QVar n) (p # n)) (QVarInstances p # n) (Map (QVar n) (p # n))
-> Map (QVar n) (p # n)
forall s a. s -> Getting a s a -> a
^. Getting
  (Map (QVar n) (p # n)) (QVarInstances p # n) (Map (QVar n) (p # n))
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
       (typ :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances))

instance
    (RTraversable typ, HTraversable (NomVarTypes typ)) =>
    HTraversable (LoadedNominalDecl typ) where
    {-# INLINE hsequence #-}
    hsequence :: (LoadedNominalDecl typ # ContainedH f p)
-> f (LoadedNominalDecl typ # p)
hsequence (LoadedNominalDecl NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
p NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
f GTerm (GetHyperType ('AHyperType (ContainedH f p))) # typ
t) =
        NomVarTypes typ ('AHyperType (QVarInstances p))
-> NomVarTypes typ ('AHyperType (QVarInstances p))
-> GTerm p ('AHyperType typ)
-> LoadedNominalDecl typ # p
forall (typ :: HyperType) (v :: AHyperType).
(NomVarTypes typ # QVarInstances (GetHyperType v))
-> (NomVarTypes typ # QVarInstances (GetHyperType v))
-> (GTerm (GetHyperType v) # typ)
-> LoadedNominalDecl typ v
LoadedNominalDecl
        (NomVarTypes typ ('AHyperType (QVarInstances p))
 -> NomVarTypes typ ('AHyperType (QVarInstances p))
 -> GTerm p ('AHyperType typ)
 -> LoadedNominalDecl typ # p)
-> f (NomVarTypes typ ('AHyperType (QVarInstances p)))
-> f (NomVarTypes typ ('AHyperType (QVarInstances p))
      -> GTerm p ('AHyperType typ) -> LoadedNominalDecl typ # p)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NomVarTypes typ # QVarInstances (ContainedH f p))
-> f (NomVarTypes typ ('AHyperType (QVarInstances p)))
forall (h2 :: HyperType).
(NomVarTypes typ # QVarInstances (ContainedH f h2))
-> f (NomVarTypes typ # QVarInstances h2)
onMap NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
NomVarTypes typ # QVarInstances (ContainedH f p)
p
        f (NomVarTypes typ ('AHyperType (QVarInstances p))
   -> GTerm p ('AHyperType typ) -> LoadedNominalDecl typ # p)
-> f (NomVarTypes typ ('AHyperType (QVarInstances p)))
-> f (GTerm p ('AHyperType typ) -> LoadedNominalDecl typ # p)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (NomVarTypes typ # QVarInstances (ContainedH f p))
-> f (NomVarTypes typ ('AHyperType (QVarInstances p)))
forall (h2 :: HyperType).
(NomVarTypes typ # QVarInstances (ContainedH f h2))
-> f (NomVarTypes typ # QVarInstances h2)
onMap NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
NomVarTypes typ # QVarInstances (ContainedH f p)
f
        f (GTerm p ('AHyperType typ) -> LoadedNominalDecl typ # p)
-> f (GTerm p ('AHyperType typ)) -> f (LoadedNominalDecl typ # p)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((HFlip GTerm typ # ContainedH f p) -> f (HFlip GTerm typ # p))
-> (GTerm (ContainedH f p) # typ) -> f (GTerm p ('AHyperType typ))
forall (f0 :: HyperType -> HyperType) (k0 :: HyperType)
       (x0 :: HyperType) (f1 :: HyperType -> HyperType) (k1 :: HyperType)
       (x1 :: HyperType).
Iso (f0 k0 # x0) (f1 k1 # x1) (HFlip f0 x0 # k0) (HFlip f1 x1 # k1)
hflipped (HFlip GTerm typ # ContainedH f p) -> f (HFlip GTerm typ # p)
forall (h :: HyperType) (f :: * -> *) (p :: HyperType).
(HTraversable h, Applicative f) =>
(h # ContainedH f p) -> f (h # p)
hsequence GTerm (GetHyperType ('AHyperType (ContainedH f p))) # typ
GTerm (ContainedH f p) # typ
t
        where
            onMap :: (NomVarTypes typ # QVarInstances (ContainedH f h2))
-> f (NomVarTypes typ # QVarInstances h2)
onMap = (forall (n :: HyperType).
 HWitness (NomVarTypes typ) n
 -> (QVarInstances (ContainedH f h2) # n)
 -> f (QVarInstances h2 # n))
-> (NomVarTypes typ # QVarInstances (ContainedH f h2))
-> f (NomVarTypes typ # QVarInstances h2)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse ((QVarInstances (ContainedH f h2) ('AHyperType n)
 -> f (QVarInstances h2 ('AHyperType n)))
-> HWitness (NomVarTypes typ) n
-> QVarInstances (ContainedH f h2) ('AHyperType n)
-> f (QVarInstances h2 ('AHyperType n))
forall a b. a -> b -> a
const (((Map (QVar n) (ContainedH f h2 ('AHyperType n))
 -> f (Map (QVar n) (h2 ('AHyperType n))))
-> QVarInstances (ContainedH f h2) ('AHyperType n)
-> f (QVarInstances h2 ('AHyperType n))
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
       (typ :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar n) (ContainedH f h2 ('AHyperType n))
  -> f (Map (QVar n) (h2 ('AHyperType n))))
 -> QVarInstances (ContainedH f h2) ('AHyperType n)
 -> f (QVarInstances h2 ('AHyperType n)))
-> ((ContainedH f h2 ('AHyperType n) -> f (h2 ('AHyperType n)))
    -> Map (QVar n) (ContainedH f h2 ('AHyperType n))
    -> f (Map (QVar n) (h2 ('AHyperType n))))
-> (ContainedH f h2 ('AHyperType n) -> f (h2 ('AHyperType n)))
-> QVarInstances (ContainedH f h2) ('AHyperType n)
-> f (QVarInstances h2 ('AHyperType n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ContainedH f h2 ('AHyperType n) -> f (h2 ('AHyperType n)))
-> Map (QVar n) (ContainedH f h2 ('AHyperType n))
-> f (Map (QVar n) (h2 ('AHyperType n)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) ContainedH f h2 ('AHyperType n) -> f (h2 ('AHyperType n))
forall (f :: * -> *) (p :: HyperType) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH))

{-# INLINE loadBody #-}
loadBody ::
    ( UnifyGen m typ
    , HNodeLens varTypes typ
    , Ord (QVar typ)
    ) =>
    varTypes # QVarInstances (UVarOf m) ->
    varTypes # QVarInstances (UVarOf m) ->
    typ # GTerm (UVarOf m) ->
    m (GTerm (UVarOf m) # typ)
loadBody :: (varTypes # QVarInstances (UVarOf m))
-> (varTypes # QVarInstances (UVarOf m))
-> (typ # GTerm (UVarOf m))
-> m (GTerm (UVarOf m) # typ)
loadBody varTypes # QVarInstances (UVarOf m)
params varTypes # QVarInstances (UVarOf m)
foralls typ # GTerm (UVarOf m)
x =
    case typ # GTerm (UVarOf m)
x (typ # GTerm (UVarOf m))
-> Getting (First (QVar typ)) (typ # GTerm (UVarOf m)) (QVar typ)
-> Maybe (QVar typ)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting (First (QVar typ)) (typ # GTerm (UVarOf m)) (QVar typ)
forall (t :: HyperType) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar Maybe (QVar typ)
-> (QVar typ -> Maybe (UVarOf m ('AHyperType typ)))
-> Maybe (UVarOf m ('AHyperType typ))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= QVar typ -> Maybe (UVarOf m ('AHyperType typ))
get of
    Just UVarOf m ('AHyperType typ)
r -> UVarOf m ('AHyperType typ) -> GTerm (UVarOf m) # typ
forall (v :: HyperType) (ast :: AHyperType). v ast -> GTerm v ast
GPoly UVarOf m ('AHyperType typ)
r (GTerm (UVarOf m) # typ)
-> ((GTerm (UVarOf m) # typ) -> m (GTerm (UVarOf m) # typ))
-> m (GTerm (UVarOf m) # typ)
forall a b. a -> (a -> b) -> b
& (GTerm (UVarOf m) # typ) -> m (GTerm (UVarOf m) # typ)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    Maybe (UVarOf m ('AHyperType typ))
Nothing ->
        case (forall (n :: HyperType).
 HWitness typ n -> (GTerm (UVarOf m) # n) -> Maybe (UVarOf m # n))
-> (typ # GTerm (UVarOf m)) -> Maybe (typ # UVarOf m)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (((GTerm (UVarOf m) # n) -> Maybe (UVarOf m # n))
-> HWitness typ n -> (GTerm (UVarOf m) # n) -> Maybe (UVarOf m # n)
forall a b. a -> b -> a
const ((GTerm (UVarOf m) # n)
-> Getting
     (First (UVarOf m # n)) (GTerm (UVarOf m) # n) (UVarOf m # n)
-> Maybe (UVarOf m # n)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting
  (First (UVarOf m # n)) (GTerm (UVarOf m) # n) (UVarOf m # n)
forall (v :: HyperType) (ast :: AHyperType).
Prism' (GTerm v ast) (v ast)
_GMono)) typ # GTerm (UVarOf m)
x of
        Just typ # UVarOf m
xm -> (typ # UVarOf m) -> m (UVarOf m ('AHyperType typ))
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm typ # UVarOf m
xm m (UVarOf m ('AHyperType typ))
-> (UVarOf m ('AHyperType typ) -> GTerm (UVarOf m) # typ)
-> m (GTerm (UVarOf m) # typ)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> UVarOf m ('AHyperType typ) -> GTerm (UVarOf m) # typ
forall (v :: HyperType) (ast :: AHyperType). v ast -> GTerm v ast
GMono
        Maybe (typ # UVarOf m)
Nothing -> ('AHyperType typ :# GTerm (UVarOf m)) -> GTerm (UVarOf m) # typ
forall (v :: HyperType) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody typ # GTerm (UVarOf m)
'AHyperType typ :# GTerm (UVarOf m)
x (GTerm (UVarOf m) # typ)
-> ((GTerm (UVarOf m) # typ) -> m (GTerm (UVarOf m) # typ))
-> m (GTerm (UVarOf m) # typ)
forall a b. a -> (a -> b) -> b
& (GTerm (UVarOf m) # typ) -> m (GTerm (UVarOf m) # typ)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    where
        get :: QVar typ -> Maybe (UVarOf m ('AHyperType typ))
get QVar typ
v =
            varTypes # QVarInstances (UVarOf m)
params (varTypes # QVarInstances (UVarOf m))
-> Getting
     (First (UVarOf m ('AHyperType typ)))
     (varTypes # QVarInstances (UVarOf m))
     (UVarOf m ('AHyperType typ))
-> Maybe (UVarOf m ('AHyperType typ))
forall s a. s -> Getting (First a) s a -> Maybe a
^? ((QVarInstances (UVarOf m) # typ)
 -> Const
      (First (UVarOf m ('AHyperType typ)))
      (QVarInstances (UVarOf m) # typ))
-> (varTypes # QVarInstances (UVarOf m))
-> Const
     (First (UVarOf m ('AHyperType typ)))
     (varTypes # QVarInstances (UVarOf m))
forall (s :: HyperType) (a :: HyperType) (h :: HyperType).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens (((QVarInstances (UVarOf m) # typ)
  -> Const
       (First (UVarOf m ('AHyperType typ)))
       (QVarInstances (UVarOf m) # typ))
 -> (varTypes # QVarInstances (UVarOf m))
 -> Const
      (First (UVarOf m ('AHyperType typ)))
      (varTypes # QVarInstances (UVarOf m)))
-> ((UVarOf m ('AHyperType typ)
     -> Const
          (First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
    -> (QVarInstances (UVarOf m) # typ)
    -> Const
         (First (UVarOf m ('AHyperType typ)))
         (QVarInstances (UVarOf m) # typ))
-> Getting
     (First (UVarOf m ('AHyperType typ)))
     (varTypes # QVarInstances (UVarOf m))
     (UVarOf m ('AHyperType typ))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (QVar typ) (UVarOf m ('AHyperType typ))
 -> Const
      (First (UVarOf m ('AHyperType typ)))
      (Map (QVar typ) (UVarOf m ('AHyperType typ))))
-> (QVarInstances (UVarOf m) # typ)
-> Const
     (First (UVarOf m ('AHyperType typ)))
     (QVarInstances (UVarOf m) # typ)
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
       (typ :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar typ) (UVarOf m ('AHyperType typ))
  -> Const
       (First (UVarOf m ('AHyperType typ)))
       (Map (QVar typ) (UVarOf m ('AHyperType typ))))
 -> (QVarInstances (UVarOf m) # typ)
 -> Const
      (First (UVarOf m ('AHyperType typ)))
      (QVarInstances (UVarOf m) # typ))
-> ((UVarOf m ('AHyperType typ)
     -> Const
          (First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
    -> Map (QVar typ) (UVarOf m ('AHyperType typ))
    -> Const
         (First (UVarOf m ('AHyperType typ)))
         (Map (QVar typ) (UVarOf m ('AHyperType typ))))
-> (UVarOf m ('AHyperType typ)
    -> Const
         (First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
-> (QVarInstances (UVarOf m) # typ)
-> Const
     (First (UVarOf m ('AHyperType typ)))
     (QVarInstances (UVarOf m) # typ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map (QVar typ) (UVarOf m ('AHyperType typ)))
-> Traversal'
     (Map (QVar typ) (UVarOf m ('AHyperType typ)))
     (IxValue (Map (QVar typ) (UVarOf m ('AHyperType typ))))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Index (Map (QVar typ) (UVarOf m ('AHyperType typ)))
QVar typ
v Maybe (UVarOf m ('AHyperType typ))
-> Maybe (UVarOf m ('AHyperType typ))
-> Maybe (UVarOf m ('AHyperType typ))
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
            varTypes # QVarInstances (UVarOf m)
foralls (varTypes # QVarInstances (UVarOf m))
-> Getting
     (First (UVarOf m ('AHyperType typ)))
     (varTypes # QVarInstances (UVarOf m))
     (UVarOf m ('AHyperType typ))
-> Maybe (UVarOf m ('AHyperType typ))
forall s a. s -> Getting (First a) s a -> Maybe a
^? ((QVarInstances (UVarOf m) # typ)
 -> Const
      (First (UVarOf m ('AHyperType typ)))
      (QVarInstances (UVarOf m) # typ))
-> (varTypes # QVarInstances (UVarOf m))
-> Const
     (First (UVarOf m ('AHyperType typ)))
     (varTypes # QVarInstances (UVarOf m))
forall (s :: HyperType) (a :: HyperType) (h :: HyperType).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens (((QVarInstances (UVarOf m) # typ)
  -> Const
       (First (UVarOf m ('AHyperType typ)))
       (QVarInstances (UVarOf m) # typ))
 -> (varTypes # QVarInstances (UVarOf m))
 -> Const
      (First (UVarOf m ('AHyperType typ)))
      (varTypes # QVarInstances (UVarOf m)))
-> ((UVarOf m ('AHyperType typ)
     -> Const
          (First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
    -> (QVarInstances (UVarOf m) # typ)
    -> Const
         (First (UVarOf m ('AHyperType typ)))
         (QVarInstances (UVarOf m) # typ))
-> Getting
     (First (UVarOf m ('AHyperType typ)))
     (varTypes # QVarInstances (UVarOf m))
     (UVarOf m ('AHyperType typ))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (QVar typ) (UVarOf m ('AHyperType typ))
 -> Const
      (First (UVarOf m ('AHyperType typ)))
      (Map (QVar typ) (UVarOf m ('AHyperType typ))))
-> (QVarInstances (UVarOf m) # typ)
-> Const
     (First (UVarOf m ('AHyperType typ)))
     (QVarInstances (UVarOf m) # typ)
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
       (typ :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar typ) (UVarOf m ('AHyperType typ))
  -> Const
       (First (UVarOf m ('AHyperType typ)))
       (Map (QVar typ) (UVarOf m ('AHyperType typ))))
 -> (QVarInstances (UVarOf m) # typ)
 -> Const
      (First (UVarOf m ('AHyperType typ)))
      (QVarInstances (UVarOf m) # typ))
-> ((UVarOf m ('AHyperType typ)
     -> Const
          (First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
    -> Map (QVar typ) (UVarOf m ('AHyperType typ))
    -> Const
         (First (UVarOf m ('AHyperType typ)))
         (Map (QVar typ) (UVarOf m ('AHyperType typ))))
-> (UVarOf m ('AHyperType typ)
    -> Const
         (First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
-> (QVarInstances (UVarOf m) # typ)
-> Const
     (First (UVarOf m ('AHyperType typ)))
     (QVarInstances (UVarOf m) # typ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map (QVar typ) (UVarOf m ('AHyperType typ)))
-> Traversal'
     (Map (QVar typ) (UVarOf m ('AHyperType typ)))
     (IxValue (Map (QVar typ) (UVarOf m ('AHyperType typ))))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Index (Map (QVar typ) (UVarOf m ('AHyperType typ)))
QVar typ
v

{-# INLINE loadNominalDecl #-}
loadNominalDecl ::
    forall m typ.
    ( Monad m
    , HTraversable (NomVarTypes typ)
    , HNodesConstraint (NomVarTypes typ) (Unify m)
    , HasScheme (NomVarTypes typ) m typ
    ) =>
    Pure # NominalDecl typ ->
    m (LoadedNominalDecl typ # UVarOf m)
loadNominalDecl :: (Pure # NominalDecl typ) -> m (LoadedNominalDecl typ # UVarOf m)
loadNominalDecl (Pure (NominalDecl params (Scheme foralls typ))) =
    do
        NomVarTypes typ # QVarInstances (UVarOf m)
paramsL <- (forall (n :: HyperType).
 HWitness (NomVarTypes typ) n
 -> (QVars # n) -> m (QVarInstances (UVarOf m) # n))
-> (NomVarTypes typ # QVars)
-> m (NomVarTypes typ # QVarInstances (UVarOf m))
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m) Proxy (Unify m)
-> (Unify m n => (QVars # n) -> m (QVarInstances (UVarOf m) # n))
-> HWitness (NomVarTypes typ) n
-> (QVars # n)
-> m (QVarInstances (UVarOf m) # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> Unify m n => (QVars # n) -> m (QVarInstances (UVarOf m) # n)
forall (m :: * -> *) (typ :: HyperType).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances) NomVarTypes typ # QVars
params
        NomVarTypes typ # QVarInstances (UVarOf m)
forallsL <- (forall (n :: HyperType).
 HWitness (NomVarTypes typ) n
 -> (QVars # n) -> m (QVarInstances (UVarOf m) # n))
-> (NomVarTypes typ # QVars)
-> m (NomVarTypes typ # QVarInstances (UVarOf m))
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m) Proxy (Unify m)
-> (Unify m n => (QVars # n) -> m (QVarInstances (UVarOf m) # n))
-> HWitness (NomVarTypes typ) n
-> (QVars # n)
-> m (QVarInstances (UVarOf m) # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> Unify m n => (QVars # n) -> m (QVarInstances (UVarOf m) # n)
forall (m :: * -> *) (typ :: HyperType).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances) NomVarTypes typ # QVars
foralls
        (forall (n :: HyperType).
 HRecWitness typ n
 -> (n # GTerm (UVarOf m)) -> m (GTerm (UVarOf m) # n))
-> (Pure # typ) -> m (GTerm (UVarOf m) # typ)
forall (m :: * -> *) (h :: HyperType) (w :: HyperType).
(Monad m, RTraversable h) =>
(forall (n :: HyperType). HRecWitness h n -> (n # w) -> m (w # n))
-> (Pure # h) -> m (w # h)
wrapM
            (Proxy (HasScheme (NomVarTypes typ) m)
forall k (t :: k). Proxy t
Proxy @(HasScheme (NomVarTypes typ) m) Proxy (HasScheme (NomVarTypes typ) m)
-> (HasScheme (NomVarTypes typ) m n =>
    (n # GTerm (UVarOf m)) -> m (GTerm (UVarOf m) # n))
-> HRecWitness typ n
-> (n # GTerm (UVarOf m))
-> m (GTerm (UVarOf m) # n)
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (n :: HyperType) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>>
                (NomVarTypes typ # QVarInstances (UVarOf m))
-> (NomVarTypes typ # QVarInstances (UVarOf m))
-> (n # GTerm (UVarOf m))
-> m (GTerm (UVarOf m) # n)
forall (m :: * -> *) (typ :: HyperType) (varTypes :: HyperType).
(UnifyGen m typ, HNodeLens varTypes typ, Ord (QVar typ)) =>
(varTypes # QVarInstances (UVarOf m))
-> (varTypes # QVarInstances (UVarOf m))
-> (typ # GTerm (UVarOf m))
-> m (GTerm (UVarOf m) # typ)
loadBody NomVarTypes typ # QVarInstances (UVarOf m)
paramsL NomVarTypes typ # QVarInstances (UVarOf m)
forallsL
            ) 'AHyperType Pure :# typ
Pure # typ
typ
            m (GTerm (UVarOf m) # typ)
-> ((GTerm (UVarOf m) # typ) -> LoadedNominalDecl typ # UVarOf m)
-> m (LoadedNominalDecl typ # UVarOf m)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (NomVarTypes typ
 # QVarInstances (GetHyperType ('AHyperType (UVarOf m))))
-> (NomVarTypes typ
    # QVarInstances (GetHyperType ('AHyperType (UVarOf m))))
-> (GTerm (GetHyperType ('AHyperType (UVarOf m))) # typ)
-> LoadedNominalDecl typ # UVarOf m
forall (typ :: HyperType) (v :: AHyperType).
(NomVarTypes typ # QVarInstances (GetHyperType v))
-> (NomVarTypes typ # QVarInstances (GetHyperType v))
-> (GTerm (GetHyperType v) # typ)
-> LoadedNominalDecl typ v
LoadedNominalDecl NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes typ # QVarInstances (UVarOf m)
paramsL NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes typ # QVarInstances (UVarOf m)
forallsL

class MonadNominals nomId typ m where
    getNominalDecl :: nomId -> m (LoadedNominalDecl typ # UVarOf m)

class HasNominalInst nomId typ where
    nominalInst :: Prism' (typ # h) (NominalInst nomId (NomVarTypes typ) # h)

{-# INLINE lookupParams #-}
lookupParams ::
    forall m varTypes.
    ( Applicative m
    , HTraversable varTypes
    , HNodesConstraint varTypes (UnifyGen m)
    ) =>
    varTypes # QVarInstances (UVarOf m) ->
    m (varTypes # QVarInstances (UVarOf m))
lookupParams :: (varTypes # QVarInstances (UVarOf m))
-> m (varTypes # QVarInstances (UVarOf m))
lookupParams =
    (forall (n :: HyperType).
 HWitness varTypes n
 -> (QVarInstances (UVarOf m) # n)
 -> m (QVarInstances (UVarOf m) # n))
-> (varTypes # QVarInstances (UVarOf m))
-> m (varTypes # QVarInstances (UVarOf m))
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (Proxy (UnifyGen m)
forall k (t :: k). Proxy t
Proxy @(UnifyGen m) Proxy (UnifyGen m)
-> (UnifyGen m n =>
    (QVarInstances (UVarOf m) # n) -> m (QVarInstances (UVarOf m) # n))
-> HWitness varTypes n
-> (QVarInstances (UVarOf m) # n)
-> m (QVarInstances (UVarOf m) # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> ((Map (QVar n) (UVarOf m ('AHyperType n))
 -> m (Map (QVar n) (UVarOf m ('AHyperType n))))
-> (QVarInstances (UVarOf m) # n)
-> m (QVarInstances (UVarOf m) # n)
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
       (typ :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances ((Map (QVar n) (UVarOf m ('AHyperType n))
  -> m (Map (QVar n) (UVarOf m ('AHyperType n))))
 -> (QVarInstances (UVarOf m) # n)
 -> m (QVarInstances (UVarOf m) # n))
-> ((UVarOf m ('AHyperType n) -> m (UVarOf m ('AHyperType n)))
    -> Map (QVar n) (UVarOf m ('AHyperType n))
    -> m (Map (QVar n) (UVarOf m ('AHyperType n))))
-> (UVarOf m ('AHyperType n) -> m (UVarOf m ('AHyperType n)))
-> (QVarInstances (UVarOf m) # n)
-> m (QVarInstances (UVarOf m) # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UVarOf m ('AHyperType n) -> m (UVarOf m ('AHyperType n)))
-> Map (QVar n) (UVarOf m ('AHyperType n))
-> m (Map (QVar n) (UVarOf m ('AHyperType n)))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) UVarOf m ('AHyperType n) -> m (UVarOf m ('AHyperType n))
forall (t :: HyperType).
UnifyGen m t =>
(UVarOf m # t) -> m (UVarOf m # t)
lookupParam)
    where
        lookupParam :: forall t. UnifyGen m t => UVarOf m # t -> m (UVarOf m # t)
        lookupParam :: (UVarOf m # t) -> m (UVarOf m # t)
lookupParam UVarOf m # t
v =
            BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> m (UTerm (UVarOf m) # t)
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v
            m (UTerm (UVarOf m) # t)
-> ((UTerm (UVarOf m) # t) -> m (UVarOf m # t)) -> m (UVarOf m # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
            \case
            UInstantiated UVarOf m # t
r -> (UVarOf m # t) -> m (UVarOf m # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
r
            USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l ->
                -- This is a phantom-type, wasn't instantiated by `instantiate`.
                Proxy t -> m (TypeConstraintsOf t)
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (Proxy t
forall k (t :: k). Proxy t
Proxy @t) m (TypeConstraintsOf t)
-> (TypeConstraintsOf t -> TypeConstraintsOf t)
-> m (TypeConstraintsOf t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (TypeConstraintsOf t -> TypeConstraintsOf t -> TypeConstraintsOf t
forall a. Semigroup a => a -> a -> a
<> TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
l) m (TypeConstraintsOf t)
-> (TypeConstraintsOf t -> m (UVarOf m # t)) -> m (UVarOf m # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= BindingDict (UVarOf m) m t
-> (UTerm (UVarOf m) # t) -> m (UVarOf m # t)
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding ((UTerm (UVarOf m) # t) -> m (UVarOf m # t))
-> (TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> TypeConstraintsOf t
-> m (UVarOf m # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeConstraintsOf t -> UTerm (UVarOf m) # t
forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound
            UTerm (UVarOf m) # t
_ -> String -> m (UVarOf m # t)
forall a. HasCallStack => String -> a
error String
"unexpected state at nominal's parameter"

type instance InferOf (ToNom n e) = NominalInst n (NomVarTypes (TypeOf e))

instance
    ( MonadScopeLevel m
    , MonadNominals nomId (TypeOf expr) m
    , HTraversable (NomVarTypes (TypeOf expr))
    , HNodesConstraint (NomVarTypes (TypeOf expr)) (UnifyGen m)
    , UnifyGen m (TypeOf expr)
    , HasInferredType expr
    , Infer m expr
    ) =>
    Infer m (ToNom nomId expr) where

    {-# INLINE inferBody #-}
    inferBody :: (ToNom nomId expr # InferChild m h)
-> m (ToNom nomId expr # h, InferOf (ToNom nomId expr) # UVarOf m)
inferBody (ToNom nomId
nomId 'AHyperType (InferChild m h) :# expr
val) =
        do
            (InferredChild h ('AHyperType expr)
valI InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
valR, UVarOf m # TypeOf expr
typ, NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT) <-
                do
                    InferredChild (UVarOf m) h ('AHyperType expr)
v <- InferChild m h ('AHyperType expr)
-> m (InferredChild (UVarOf m) h ('AHyperType expr))
forall (m :: * -> *) (h :: HyperType) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# expr
InferChild m h ('AHyperType expr)
val
                    LoadedNominalDecl NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
params NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
foralls GTerm (GetHyperType ('AHyperType (UVarOf m))) # TypeOf expr
gen <- nomId
-> m (LoadedNominalDecl (TypeOf expr) ('AHyperType (UVarOf m)))
forall nomId (typ :: HyperType) (m :: * -> *).
MonadNominals nomId typ m =>
nomId -> m (LoadedNominalDecl typ # UVarOf m)
getNominalDecl nomId
nomId
                    [m ()]
recover <-
                        (forall (c :: HyperType).
 HWitness (NomVarTypes (TypeOf expr)) c
 -> (QVarInstances (UVarOf m) # c) -> WriterT [m ()] m ())
-> (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> WriterT [m ()] m ()
forall (f :: * -> *) (h :: HyperType) (m :: HyperType).
(Applicative f, HFoldable h) =>
(forall (c :: HyperType). HWitness h c -> (m # c) -> f ())
-> (h # m) -> f ()
htraverse_
                        ( Proxy (UnifyGen m)
forall k (t :: k). Proxy t
Proxy @(UnifyGen m) Proxy (UnifyGen m)
-> (UnifyGen m c =>
    (QVarInstances (UVarOf m) # c) -> WriterT [m ()] m ())
-> HWitness (NomVarTypes (TypeOf expr)) c
-> (QVarInstances (UVarOf m) # c)
-> WriterT [m ()] m ()
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
                            ((UVarOf m # c) -> WriterT [m ()] m (UVarOf m # c))
-> Map (QVar c) (UVarOf m # c) -> WriterT [m ()] m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ ((TypeConstraintsOf c -> UTerm (UVarOf m) # c)
-> (UVarOf m # c) -> WriterT [m ()] m (UVarOf m # c)
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateForAll TypeConstraintsOf c -> UTerm (UVarOf m) # c
forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem) (Map (QVar c) (UVarOf m # c) -> WriterT [m ()] m ())
-> ((QVarInstances (UVarOf m) # c) -> Map (QVar c) (UVarOf m # c))
-> (QVarInstances (UVarOf m) # c)
-> WriterT [m ()] m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((QVarInstances (UVarOf m) # c)
-> Getting
     (Map (QVar c) (UVarOf m # c))
     (QVarInstances (UVarOf m) # c)
     (Map (QVar c) (UVarOf m # c))
-> Map (QVar c) (UVarOf m # c)
forall s a. s -> Getting a s a -> a
^. Getting
  (Map (QVar c) (UVarOf m # c))
  (QVarInstances (UVarOf m) # c)
  (Map (QVar c) (UVarOf m # c))
forall (h1 :: HyperType) (typ1 :: AHyperType) (h :: HyperType)
       (typ :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances)
                        ) NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
foralls
                        WriterT [m ()] m ()
-> (WriterT [m ()] m () -> m [m ()]) -> m [m ()]
forall a b. a -> (a -> b) -> b
& WriterT [m ()] m () -> m [m ()]
forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT
                    (UVarOf m # TypeOf expr
typ, NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT) <- m (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> (forall (n :: HyperType).
    TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # TypeOf expr)
-> m (UVarOf m # TypeOf expr,
      NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall (m :: * -> *) (t :: HyperType) a.
UnifyGen m t =>
m a
-> (forall (n :: HyperType).
    TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t)
-> m (UVarOf m # t, a)
instantiateWith ((NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> m (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall (m :: * -> *) (varTypes :: HyperType).
(Applicative m, HTraversable varTypes,
 HNodesConstraint varTypes (UnifyGen m)) =>
(varTypes # QVarInstances (UVarOf m))
-> m (varTypes # QVarInstances (UVarOf m))
lookupParams NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
params) forall (n :: HyperType).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound GTerm (GetHyperType ('AHyperType (UVarOf m))) # TypeOf expr
GTerm (UVarOf m) # TypeOf expr
gen
                    (InferredChild (UVarOf m) h ('AHyperType expr)
v, UVarOf m # TypeOf expr
typ, NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT) (InferredChild (UVarOf m) h ('AHyperType expr),
 UVarOf m # TypeOf expr,
 NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> m ()
-> m (InferredChild (UVarOf m) h ('AHyperType expr),
      UVarOf m # TypeOf expr,
      NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
recover
                m (InferredChild (UVarOf m) h ('AHyperType expr),
   UVarOf m # TypeOf expr,
   NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> (m (InferredChild (UVarOf m) h ('AHyperType expr),
       UVarOf m # TypeOf expr,
       NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
    -> m (InferredChild (UVarOf m) h ('AHyperType expr),
          UVarOf m # TypeOf expr,
          NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)))
-> m (InferredChild (UVarOf m) h ('AHyperType expr),
      UVarOf m # TypeOf expr,
      NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall a b. a -> (a -> b) -> b
& m (InferredChild (UVarOf m) h ('AHyperType expr),
   UVarOf m # TypeOf expr,
   NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> m (InferredChild (UVarOf m) h ('AHyperType expr),
      UVarOf m # TypeOf expr,
      NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel
            (nomId -> ('AHyperType h :# expr) -> ToNom nomId expr # h
forall nomId (term :: HyperType) (h :: AHyperType).
nomId -> (h :# term) -> ToNom nomId term h
ToNom nomId
nomId h ('AHyperType expr)
'AHyperType h :# expr
valI, nomId
-> (NomVarTypes (TypeOf expr)
    # QVarInstances (GetHyperType ('AHyperType (UVarOf m))))
-> NominalInst
     nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m))
forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
nomId NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT)
                (ToNom nomId expr # h,
 NominalInst
   nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m)))
-> m (UVarOf m # TypeOf expr)
-> m (ToNom nomId expr # h,
      NominalInst
        nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m)))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (UVarOf m # TypeOf expr)
-> (UVarOf m # TypeOf expr) -> m (UVarOf m # TypeOf expr)
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> (UVarOf m # t) -> m (UVarOf m # t)
unify UVarOf m # TypeOf expr
typ (InferOf expr ('AHyperType (UVarOf m))
InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
valR InferOf expr ('AHyperType (UVarOf m))
-> ALens
     (InferOf expr ('AHyperType (UVarOf m)))
     (InferOf expr ('AHyperType (UVarOf m)))
     (UVarOf m # TypeOf expr)
     (UVarOf m # TypeOf expr)
-> UVarOf m # TypeOf expr
forall s t a b. s -> ALens s t a b -> a
^# Proxy expr
-> ALens
     (InferOf expr ('AHyperType (UVarOf m)))
     (InferOf expr ('AHyperType (UVarOf m)))
     (UVarOf m # TypeOf expr)
     (UVarOf m # TypeOf expr)
forall (t :: HyperType) (v :: HyperType).
HasInferredType t =>
Proxy t -> ALens' (InferOf t # v) (v # TypeOf t)
inferredType (Proxy expr
forall k (t :: k). Proxy t
Proxy @expr))

type instance InferOf (FromNom _ e) = FuncType (TypeOf e)

instance
    ( Infer m expr
    , HasNominalInst nomId (TypeOf expr)
    , MonadNominals nomId (TypeOf expr) m
    , HTraversable (NomVarTypes (TypeOf expr))
    , HNodesConstraint (NomVarTypes (TypeOf expr)) (UnifyGen m)
    , UnifyGen m (TypeOf expr)
    ) =>
    Infer m (FromNom nomId expr) where

    {-# INLINE inferBody #-}
    inferBody :: (FromNom nomId expr # InferChild m h)
-> m (FromNom nomId expr # h,
      InferOf (FromNom nomId expr) # UVarOf m)
inferBody (FromNom nomId
nomId) =
        do
            LoadedNominalDecl NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
params NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
_ GTerm (GetHyperType ('AHyperType (UVarOf m))) # TypeOf expr
gen <- nomId
-> m (LoadedNominalDecl (TypeOf expr) ('AHyperType (UVarOf m)))
forall nomId (typ :: HyperType) (m :: * -> *).
MonadNominals nomId typ m =>
nomId -> m (LoadedNominalDecl typ # UVarOf m)
getNominalDecl nomId
nomId
            (UVarOf m # TypeOf expr
typ, NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT) <- m (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> (forall (n :: HyperType).
    TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # TypeOf expr)
-> m (UVarOf m # TypeOf expr,
      NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall (m :: * -> *) (t :: HyperType) a.
UnifyGen m t =>
m a
-> (forall (n :: HyperType).
    TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t)
-> m (UVarOf m # t, a)
instantiateWith ((NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
-> m (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
forall (m :: * -> *) (varTypes :: HyperType).
(Applicative m, HTraversable varTypes,
 HNodesConstraint varTypes (UnifyGen m)) =>
(varTypes # QVarInstances (UVarOf m))
-> m (varTypes # QVarInstances (UVarOf m))
lookupParams NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
params) forall (n :: HyperType).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound GTerm (GetHyperType ('AHyperType (UVarOf m))) # TypeOf expr
GTerm (UVarOf m) # TypeOf expr
gen
            Tagged
  (NominalInst
     nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m)))
  (Identity
     (NominalInst
        nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m))))
-> Tagged
     (TypeOf expr # UVarOf m) (Identity (TypeOf expr # UVarOf m))
forall nomId (typ :: HyperType) (h :: HyperType).
HasNominalInst nomId typ =>
Prism' (typ # h) (NominalInst nomId (NomVarTypes typ) # h)
nominalInst (Tagged
   (NominalInst
      nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m)))
   (Identity
      (NominalInst
         nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m))))
 -> Tagged
      (TypeOf expr # UVarOf m) (Identity (TypeOf expr # UVarOf m)))
-> NominalInst
     nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m))
-> TypeOf expr # UVarOf m
forall t b. AReview t b -> b -> t
# nomId
-> (NomVarTypes (TypeOf expr)
    # QVarInstances (GetHyperType ('AHyperType (UVarOf m))))
-> NominalInst
     nomId (NomVarTypes (TypeOf expr)) ('AHyperType (UVarOf m))
forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
nomId NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT (TypeOf expr # UVarOf m)
-> ((TypeOf expr # UVarOf m) -> m (UVarOf m # TypeOf expr))
-> m (UVarOf m # TypeOf expr)
forall a b. a -> (a -> b) -> b
& (TypeOf expr # UVarOf m) -> m (UVarOf m # TypeOf expr)
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm
                m (UVarOf m # TypeOf expr)
-> ((UVarOf m # TypeOf expr)
    -> FuncType (TypeOf expr) ('AHyperType (UVarOf m)))
-> m (FuncType (TypeOf expr) ('AHyperType (UVarOf m)))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (('AHyperType (UVarOf m) :# TypeOf expr)
-> ('AHyperType (UVarOf m) :# TypeOf expr)
-> FuncType (TypeOf expr) ('AHyperType (UVarOf m))
forall (typ :: HyperType) (h :: AHyperType).
(h :# typ) -> (h :# typ) -> FuncType typ h
`FuncType` 'AHyperType (UVarOf m) :# TypeOf expr
UVarOf m # TypeOf expr
typ)
        m (FuncType (TypeOf expr) ('AHyperType (UVarOf m)))
-> (FuncType (TypeOf expr) ('AHyperType (UVarOf m))
    -> (FromNom nomId expr # h,
        FuncType (TypeOf expr) ('AHyperType (UVarOf m))))
-> m (FromNom nomId expr # h,
      FuncType (TypeOf expr) ('AHyperType (UVarOf m)))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (nomId -> FromNom nomId expr # h
forall nomId (term :: HyperType) (h :: AHyperType).
nomId -> FromNom nomId term h
FromNom nomId
nomId, )