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

-- | Nominal (named) types declaration, instantiation, construction, and access.
module Hyper.Syntax.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.Writer (WriterT (..), 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.Syntax.FuncType (FuncType (..))
import Hyper.Syntax.Map (TermMap (..), _TermMap)
import Hyper.Syntax.Scheme
import Hyper.Unify
import Hyper.Unify.Generalize (GTerm (..), instantiate, instantiateForAll, instantiateWith, _GMono)
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
    { forall (typ :: HyperType) (h :: AHyperType).
NominalDecl typ h -> NomVarTypes typ # QVars
_nParams :: NomVarTypes typ # QVars
    , forall (typ :: HyperType) (h :: AHyperType).
NominalDecl typ h -> Scheme (NomVarTypes typ) typ h
_nScheme :: Scheme (NomVarTypes typ) typ h
    }
    deriving (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
    { forall nomId (varTypes :: HyperType) (h :: AHyperType).
NominalInst nomId varTypes h -> nomId
_nId :: nomId
    , forall nomId (varTypes :: HyperType) (h :: AHyperType).
NominalInst nomId varTypes h
-> varTypes # QVarInstances (GetHyperType h)
_nArgs :: varTypes # QVarInstances (GetHyperType h)
    }
    deriving (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
    { forall nomId (term :: HyperType) (h :: AHyperType).
ToNom nomId term h -> nomId
_tnId :: nomId
    , forall nomId (term :: HyperType) (h :: AHyperType).
ToNom nomId term h -> h :# term
_tnVal :: h :# term
    }
    deriving (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
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, 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
Ord, Get (FromNom nomId term h)
[FromNom nomId term h] -> Put
FromNom nomId term h -> Put
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 -> ()
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
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 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
    { forall (typ :: HyperType) (v :: AHyperType).
LoadedNominalDecl typ v
-> NomVarTypes typ # QVarInstances (GetHyperType v)
lnParams :: NomVarTypes typ # QVarInstances (GetHyperType v)
    , forall (typ :: HyperType) (v :: AHyperType).
LoadedNominalDecl typ v
-> NomVarTypes typ # QVarInstances (GetHyperType v)
lnForalls :: NomVarTypes typ # QVarInstances (GetHyperType v)
    , forall (typ :: HyperType) (v :: AHyperType).
LoadedNominalDecl typ v -> GTerm (GetHyperType v) # typ
lnType :: GTerm (GetHyperType v) # typ
    }
    deriving (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 :: forall (c :: HyperType -> Constraint) (n :: HyperType) r.
HNodesConstraint (NominalInst n v) c =>
HWitness (NominalInst n v) n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitness HWitnessType (NominalInst n v) n
w) = 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 (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType (NominalInst n v) n
w)

instance HFunctor v => HFunctor (NominalInst n v) where
    {-# INLINE hmap #-}
    hmap :: forall (p :: HyperType) (q :: HyperType).
(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 = 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 forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ 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) -> forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => Setter (f a) (f b) a b
Lens.mapped forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> q # n
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType v n
w))

instance HFoldable v => HFoldable (NominalInst n v) where
    {-# INLINE hfoldMap #-}
    hfoldMap :: forall a (p :: HyperType).
Monoid a =>
(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 (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) -> forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (n :: HyperType).
HWitness (NominalInst n v) n -> (p # n) -> a
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HWitnessType v n
w)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. 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 :: forall (f :: * -> *) (p :: HyperType).
Applicative f =>
(NominalInst n v # ContainedH f p) -> f (NominalInst n v # p)
hsequence (NominalInst n
n v # QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
v) =
        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 (forall a b. a -> b -> a
const (forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances (forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall (f :: * -> *) (p :: HyperType) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH))) v # QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
v
            forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> 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 :: forall (p :: HyperType) (q :: HyperType).
(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 forall a. Eq a => a -> a -> Bool
/= nomId
yId = forall a. Maybe a
Nothing
        | Bool
otherwise =
            forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
ZipMatch h =>
(h # p) -> (h # q) -> Maybe (h # (p :*: q))
zipMatch varTypes # QVarInstances (GetHyperType ('AHyperType p))
x varTypes # QVarInstances (GetHyperType ('AHyperType q))
y
                forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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
                    ( forall {k} (t :: k). Proxy t
Proxy @ZipMatch 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
#*#
                        forall {k} (t :: k). Proxy t
Proxy @OrdQVar 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) ->
                                forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
ZipMatch h =>
(h # p) -> (h # q) -> Maybe (h # (p :*: q))
zipMatch (forall h (expr :: HyperType) (f :: AHyperType).
Map h (f :# expr) -> TermMap h expr f
TermMap Map (QVar (GetHyperType ('AHyperType n))) (p ('AHyperType n))
c0) (forall h (expr :: HyperType) (f :: AHyperType).
Map h (f :# expr) -> TermMap h expr f
TermMap Map (QVar (GetHyperType ('AHyperType n))) (q ('AHyperType n))
c1)
                                    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (h :: HyperType) (typ :: AHyperType).
Map (QVar (GetHyperType typ)) (h typ) -> QVarInstances h typ
QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. 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)
                    )
                forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> 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 :: forall (p :: HyperType).
(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) =
        forall (h :: HyperType) (p :: HyperType).
HContext h =>
(h # p) -> h # (HFunc p (Const (h # p)) :*: p)
hcontext varTypes # QVarInstances (GetHyperType ('AHyperType p))
args
            forall a b. a -> (a -> b) -> b
& forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
                ( forall {k} (t :: k). Proxy t
Proxy @OrdQVar 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
                            forall a b. a -> (a -> b) -> b
& forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances
                                forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall i (f :: * -> *) a b.
FunctorWithIndex i f =>
IndexedSetter i (f a) (f b) a b
Lens.imapped
                                forall i s t a b.
AnIndexedSetter i s t a b -> (i -> a -> b) -> s -> t
%@~ \QVar n
k p ('AHyperType n)
v ->
                                    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
                                                forall a b. a -> (a -> b) -> b
& forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
Lens.at QVar n
k forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ p ('AHyperType n)
newV
                                                forall a b. a -> (a -> b) -> b
& QVarInstances p ('AHyperType n)
-> Const (varTypes # QVarInstances p) ('AHyperType n)
c
                                                forall a b. a -> (a -> b) -> b
& forall {k} a (b :: k). Const a b -> a
getConst
                                                forall a b. a -> (a -> b) -> b
& forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
n
                                                forall a b. a -> (a -> b) -> b
& forall {k} a (b :: k). a -> Const a b
Const
                                        )
                                        forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: p ('AHyperType n)
v
                )
            forall a b. a -> (a -> b) -> b
& 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 GetHyperType h ('AHyperType term)
term) =
        (forall a. Pretty a => a -> Doc
pPrint nomId
nomId forall a. Semigroup a => a -> a -> a
<> String -> Doc
P.text String
"#") Doc -> Doc -> Doc
P.<+> forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
11 GetHyperType h ('AHyperType term)
term
            forall a b. a -> (a -> b) -> b
& Bool -> Doc -> Doc
maybeParens (Rational
p 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) =
        forall a. Pretty a => a -> Doc
pPrint nomId
n
            forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
joinArgs
                (forall (h :: HyperType) a (p :: HyperType).
(HFoldable h, Monoid a) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (forall {k} (t :: k). Proxy t
Proxy @(PrettyConstraints h) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall {h :: HyperType} {typ :: AHyperType}.
(Pretty (h typ), Pretty (QVar (GetHyperType typ))) =>
QVarInstances h typ -> [Doc]
mkArgs) varTypes # QVarInstances (GetHyperType h)
vars)
        where
            joinArgs :: [Doc] -> Doc
joinArgs [] = forall a. Monoid a => a
mempty
            joinArgs [Doc]
xs = String -> Doc
P.text String
"[" forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
P.sep (Doc -> [Doc] -> [Doc]
P.punctuate (String -> Doc
P.text String
",") [Doc]
xs) 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 forall s i a. s -> IndexedGetting i (Endo [(i, a)]) s a -> [(i, a)]
^@.. forall i (t :: * -> *) a b.
TraversableWithIndex i t =>
IndexedTraversal i (t a) (t b) a b
Lens.itraversed
                    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \(QVar (GetHyperType typ)
h, h typ
v) ->
                        (forall a. Pretty a => a -> Doc
pPrint QVar (GetHyperType typ)
h forall a. Semigroup a => a -> a -> a
<> String -> Doc
P.text String
":") Doc -> Doc -> Doc
P.<+> 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 :: forall (c :: HyperType -> Constraint) (n :: HyperType) r.
HNodesConstraint (LoadedNominalDecl t) c =>
HWitness (LoadedNominalDecl t) n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitness (E_LoadedNominalDecl_Body HRecWitness t n
w)) = 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 _) (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness HRecWitness t n
w)
    hLiftConstraint (HWitness (E_LoadedNominalDecl_NomVarTypes HWitness (NomVarTypes t) n
w)) = 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 (p :: HyperType) (q :: HyperType).
(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) =
        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 (GetHyperType ('AHyperType p))
mp)
            ((NomVarTypes typ # QVarInstances p)
-> NomVarTypes typ # QVarInstances q
onMap NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mf)
            (GTerm (GetHyperType ('AHyperType p)) # typ
t forall a b. a -> (a -> b) -> b
& 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 forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ 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) -> forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (forall (t :: HyperType) (n :: HyperType).
HRecWitness t n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_Body HWitnessType (HFlip GTerm typ) n
w))))
        where
            onMap :: (NomVarTypes typ # QVarInstances p)
-> NomVarTypes typ # QVarInstances q
onMap = 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 -> forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => Setter (f a) (f b) a b
Lens.mapped forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> q # n
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (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 a (p :: HyperType).
Monoid a =>
(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 (GetHyperType ('AHyperType p))
mp
            forall a. Semigroup a => a -> a -> a
<> (NomVarTypes typ # QVarInstances p) -> a
onMap NomVarTypes typ # QVarInstances (GetHyperType ('AHyperType p))
mf
            forall a. Semigroup a => a -> a -> 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) -> forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (forall (t :: HyperType) (n :: HyperType).
HRecWitness t n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_Body HWitnessType (HFlip GTerm typ) n
w))) (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 forall t b. AReview t b -> b -> t
# GTerm (GetHyperType ('AHyperType p)) # typ
t)
        where
            onMap :: (NomVarTypes typ # QVarInstances p) -> a
onMap =
                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 ->
                        forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (n :: HyperType).
HWitness (LoadedNominalDecl typ) n -> (p # n) -> a
f (forall (h :: HyperType) (n :: HyperType).
HWitnessType h n -> HWitness h n
HWitness (forall (t :: HyperType) (n :: HyperType).
HWitness (NomVarTypes t) n -> W_LoadedNominalDecl t n
E_LoadedNominalDecl_NomVarTypes HWitness (NomVarTypes typ) n
w)))
                            forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances)
                    )

instance
    (RTraversable typ, HTraversable (NomVarTypes typ)) =>
    HTraversable (LoadedNominalDecl typ)
    where
    {-# INLINE hsequence #-}
    hsequence :: forall (f :: * -> *) (p :: HyperType).
Applicative f =>
(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) =
        forall (typ :: HyperType) (v :: AHyperType).
(NomVarTypes typ # QVarInstances (GetHyperType v))
-> (NomVarTypes typ # QVarInstances (GetHyperType v))
-> (GTerm (GetHyperType v) # typ)
-> LoadedNominalDecl typ v
LoadedNominalDecl
            forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {p :: HyperType}.
(NomVarTypes typ # QVarInstances (ContainedH f p))
-> f (NomVarTypes typ # QVarInstances p)
onMap NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
p
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall {p :: HyperType}.
(NomVarTypes typ # QVarInstances (ContainedH f p))
-> f (NomVarTypes typ # QVarInstances p)
onMap NomVarTypes typ
# QVarInstances (GetHyperType ('AHyperType (ContainedH f p)))
f
            forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 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
t
        where
            onMap :: (NomVarTypes typ # QVarInstances (ContainedH f p))
-> f (NomVarTypes typ # QVarInstances p)
onMap = 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 (forall a b. a -> b -> a
const ((forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) 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 :: 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 varTypes # QVarInstances (UVarOf m)
params varTypes # QVarInstances (UVarOf m)
foralls typ # GTerm (UVarOf m)
x =
    case typ # GTerm (UVarOf m)
x forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (t :: HyperType) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar 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 -> forall (v :: HyperType) (ast :: AHyperType). v ast -> GTerm v ast
GPoly UVarOf m ('AHyperType typ)
r forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a. Applicative f => a -> f a
pure
        Maybe (UVarOf m ('AHyperType typ))
Nothing ->
            case 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 (forall a b. a -> b -> a
const (forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (v :: HyperType) (ast :: AHyperType).
Prism' (GTerm v ast) (v ast)
_GMono)) typ # GTerm (UVarOf m)
x of
                Just typ # UVarOf m
xm -> forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm typ # UVarOf m
xm forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: HyperType) (ast :: AHyperType). v ast -> GTerm v ast
GMono
                Maybe (typ # UVarOf m)
Nothing -> forall (v :: HyperType) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody typ # GTerm (UVarOf m)
x forall a b. a -> (a -> b) -> b
& 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 forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (s :: HyperType) (a :: HyperType) (h :: HyperType).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix QVar typ
v
                forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> varTypes # QVarInstances (UVarOf m)
foralls forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (s :: HyperType) (a :: HyperType) (h :: HyperType).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix QVar typ
v

{-# INLINE loadNominalDecl #-}
loadNominalDecl ::
    forall m typ.
    ( HTraversable (NomVarTypes typ)
    , HNodesConstraint (NomVarTypes typ) (Unify m)
    , HasScheme (NomVarTypes typ) m typ
    ) =>
    Pure # NominalDecl typ ->
    m (LoadedNominalDecl typ # UVarOf m)
loadNominalDecl :: forall (m :: * -> *) (typ :: HyperType).
(HTraversable (NomVarTypes typ),
 HNodesConstraint (NomVarTypes typ) (Unify m),
 HasScheme (NomVarTypes typ) m typ) =>
(Pure # NominalDecl typ) -> m (LoadedNominalDecl typ # UVarOf m)
loadNominalDecl (Pure (NominalDecl NomVarTypes typ # QVars
params (Scheme NomVarTypes typ # QVars
foralls 'AHyperType Pure :# typ
typ))) =
    do
        NomVarTypes typ # QVarInstances (UVarOf m)
paramsL <- 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 (forall {k} (t :: k). Proxy t
Proxy @(Unify m) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> 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 (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 (forall {k} (t :: k). Proxy t
Proxy @(Unify m) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (m :: * -> *) (typ :: HyperType).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances) NomVarTypes typ # QVars
foralls
        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
            ( forall {k} (t :: k). Proxy t
Proxy @(HasScheme (NomVarTypes typ) m) forall (c :: HyperType -> Constraint) (h :: HyperType)
       (n :: HyperType) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>>
                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
typ
            forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> 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 (UVarOf m)
paramsL 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)

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 :: forall (h :: HyperType).
(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
            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 <- forall nomId (typ :: HyperType) (m :: * -> *).
MonadNominals nomId typ m =>
nomId -> m (LoadedNominalDecl typ # UVarOf m)
getNominalDecl nomId
nomId

            -- Setup forall variables to instantiate to skolems.
            -- This means they aren't allow to be be unified,
            -- nor to propagate to outer scope.
            [m ()]
recoverForAlls <-
                forall (f :: * -> *) (h :: HyperType) (m :: HyperType).
(Applicative f, HFoldable h) =>
(forall (c :: HyperType). HWitness h c -> (m # c) -> f ())
-> (h # m) -> f ()
htraverse_
                    ( forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
                        forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ (forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateForAll forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances)
                    )
                    NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
foralls
                    forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) w a. Monad m => WriterT w m a -> m w
execWriterT
            -- Setup params in outer scope
            (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT, [m ()]
recoverParams) <-
                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
                    ( forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
                        (forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) (forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateForAll forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound)
                    )
                    NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
params
                    forall a b. a -> (a -> b) -> b
& forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT

            UVarOf m # TypeOf expr
typ <- forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(GTerm (UVarOf m) # t) -> m (UVarOf m # t)
instantiate GTerm (GetHyperType ('AHyperType (UVarOf m))) # TypeOf expr
gen forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel

            -- Restore loaded nominal to original reusable state
            forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ([m ()]
recoverParams forall a. Semigroup a => a -> a -> a
<> [m ()]
recoverForAlls)

            -- Term within is in inner level
            InferredChild h ('AHyperType expr)
valI InferOf (GetHyperType ('AHyperType expr)) # UVarOf m
valR <- forall (m :: * -> *) (h :: HyperType) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# expr
val forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) a. MonadScopeLevel m => m a -> m a
localLevel

            -- Unify the inner term's type with the type inside the nominal
            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 (GetHyperType ('AHyperType expr)) # UVarOf m
valR forall s t a b. s -> ALens s t a b -> a
^# forall (t :: HyperType) (v :: HyperType).
HasInferredType t =>
Proxy t -> ALens' (InferOf t # v) (v # TypeOf t)
inferredType (forall {k} (t :: k). Proxy t
Proxy @expr))
            forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall nomId (term :: HyperType) (h :: AHyperType).
nomId -> (h :# term) -> ToNom nomId term h
ToNom nomId
nomId h ('AHyperType expr)
valI, forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
nomId NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT)

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 :: forall (h :: HyperType).
(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) <- forall nomId (typ :: HyperType) (m :: * -> *).
MonadNominals nomId typ m =>
nomId -> m (LoadedNominalDecl typ # UVarOf m)
getNominalDecl nomId
nomId
            let lookupParams :: m (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
lookupParams = 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 (forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (forall (h1 :: HyperType) (typ1 :: AHyperType) (h2 :: HyperType)
       (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse) forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(UVarOf m # t) -> m (UVarOf m # t)
lookupParam) NomVarTypes (TypeOf expr)
# QVarInstances (GetHyperType ('AHyperType (UVarOf m)))
params
            (UVarOf m # TypeOf expr
typ, NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT) <- 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 m (NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m))
lookupParams forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound GTerm (GetHyperType ('AHyperType (UVarOf m))) # TypeOf expr
gen
            forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm (forall nomId (typ :: HyperType) (h :: HyperType).
HasNominalInst nomId typ =>
Prism' (typ # h) (NominalInst nomId (NomVarTypes typ) # h)
nominalInst forall t b. AReview t b -> b -> t
# forall nomId (varTypes :: HyperType) (h :: AHyperType).
nomId
-> (varTypes # QVarInstances (GetHyperType h))
-> NominalInst nomId varTypes h
NominalInst nomId
nomId NomVarTypes (TypeOf expr) # QVarInstances (UVarOf m)
paramsT)
                forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall nomId (term :: HyperType) (h :: AHyperType).
nomId -> FromNom nomId term h
FromNom nomId
nomId,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (typ :: HyperType) (h :: AHyperType).
(h :# typ) -> (h :# typ) -> FuncType typ h
`FuncType` UVarOf m # TypeOf expr
typ)

lookupParam :: forall m t. UnifyGen m t => UVarOf m # t -> m (UVarOf m # t)
lookupParam :: forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
(UVarOf m # t) -> m (UVarOf m # t)
lookupParam UVarOf m # t
v =
    forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            UInstantiated UVarOf m # t
r -> 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`.
                forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (forall {k} (t :: k). Proxy t
Proxy @t) forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall a. Semigroup a => a -> a -> a
<> TypeConstraintsOf (GetHyperType ('AHyperType t))
l) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v :: HyperType) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound
            UTerm (UVarOf m) # t
_ -> forall a. HasCallStack => String -> a
error String
"unexpected state at nominal's parameter"