Various clean-ups, fix PForall(N)

- Rename PForallN to PForall.
- Rename PForall and PSome to PForall1 and PSome1.
- Fix dichotomy in handling of PType and `a PHsEf`. This was much more
  essential than initially assumed, notably, blocking on whether something
  was PType or `a PHsEf` or not would have downstream consequences that would
	result in incomprehensible errors.
- Support PSome1 in Nix backend.
- Remove Plutarch.Experimental.
- Use pforall wherever possible in the Nix example.

Examples/Nix.hs

@@ -4,14 +4,13 @@ module Examples.Nix (example) where
 
 import Data.Functor.Identity (runIdentity)
 import Data.Proxy (Proxy (Proxy))
-import Data.Text (Text, unpack)
+import Data.Text (Text)
 import Plutarch.Backends.Nix (compileAp)
 import Plutarch.Frontends.Data (PAny)
 import Plutarch.Frontends.Nix (PNix)
 import Plutarch.Prelude
-import Plutarch.PType (pHs_inverse, PHsEf)
-import Plutarch.Repr.Primitive (PReprPrimitive)
-import Plutarch.Helpers (pforall, PForallNClass, PForallN(PForallN), PForallNF(PForallNF))
+import Plutarch.PType (pHs_inverse)
+import Plutarch.Helpers (pforall, PForall, PForallF(PForallF))
 import Data.Type.Equality ((:~:)(Refl))
 
 data PMyTriple a b c ef = PMyTriple
@@ -35,14 +34,14 @@ data PProxy a b ef = PProxy
   deriving stock (Generic)
   deriving anyclass (PHasRepr)
 
-pproxy :: forall e k. (PNix e, IsPType e k) => Term e (PForallN (PProxy @k))
-pproxy = case pHs_inverse @k of Refl -> pcon $ PForallN $ pcon $ PForall $ pcon $ PForallNF $ pcon $ PForallN $ pcon $ PForall $ pcon $ PForallNF $ pcon $ PProxy
+pproxy :: forall e k. (PNix e, IsPType e k) => Term e (PForall (PProxy @k))
+pproxy = case pHs_inverse @k of Refl -> pforall $ pcon PProxy
 
 newtype PConstF a b ef = PConstF (ef /$ a #-> b #-> a)
   deriving stock (Generic)
   deriving anyclass (PHasRepr)
 
-pconst :: (PNix e) => Term e (PForallN PConstF)
+pconst :: (PNix e) => Term e (PForall PConstF)
 pconst = pforall $ pcon $ PConstF $ plam \x _y -> x
 
 pmutate :: PNix e => Term e (PMyTriple PAny PAny PAny #-> PMyTriple PAny PAny PAny)
@@ -64,7 +63,7 @@ newtype PVoidF a ef = PVoidF (ef /$ PMyVoid #-> a)
   deriving anyclass (PHasRepr)
 
 pvoid :: (PNix e) => Term e (PForall PVoidF)
-pvoid = pcon $ PForall $ pcon $ PVoidF $ plam \x -> pmatch x \case {}
+pvoid = pforall $ pcon $ PVoidF $ plam \x -> pmatch x \case {}
 
 newtype PMyUnit ef = PMyUnit (ef /$ PUnit)
   deriving stock (Generic)
@@ -75,16 +74,20 @@ newtype PTopF a ef = PTopF (ef /$ a #-> PMyUnit)
   deriving anyclass (PHasRepr)
 
 ptop :: (PNix e) => Term e (PForall PTopF)
-ptop = pcon $ PForall $ pcon $ PTopF $ plam $ const $$ PMyUnit $ pcon PUnit
+ptop = pforall $ pcon $ PTopF $ plam $ const $$ PMyUnit $$ PUnit
+
+psometop :: (PNix e) => Term e (PSome1 PTopF)
+psometop = pcon $ PSome1 Proxy $ pcon $ PTopF $ plam \(_ :: T PUnit) -> pcon $ PMyUnit $$ PUnit
 
 data PLib ef = PLib
   -- FIXME: replace with foralls
   { pmutate :: ef /$ PMyTriple PAny PAny PAny #-> PMyTriple PAny PAny PAny
-  , pconst :: ef /$ PForallN PConstF
+  , pconst :: ef /$ PForall PConstF
   , pswap :: ef /$ PMyEither PAny PAny #-> PMyEither PAny PAny
   , pvoid :: ef /$ PForall PVoidF
   , ptop :: ef /$ PForall PTopF
-  , pproxy :: ef /$ PForallN (PProxy @PUnit)
+  , pproxy :: ef /$ PForall (PProxy @PUnit)
+  , psometop :: ef /$ PSome1 PTopF
   }
   deriving stock (Generic)
   deriving anyclass (PHasRepr)
@@ -99,10 +102,8 @@ plib =
       , pvoid
       , ptop
       , pproxy
+      , psometop
       }
 
 example :: Text
 example = runIdentity $ compileAp (Proxy @PLib) plib
-
-p :: IO ()
-p = putStrLn $ unpack $ example

Plutarch/Backends/Nix.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE NondecreasingIndentation #-}
 
 module Plutarch.Backends.Nix (compileAp, compileTy) where
 
@@ -13,6 +14,7 @@ import Data.Proxy (Proxy (Proxy))
 import Data.String (fromString)
 import Data.Text (Text, pack)
 import Data.Text.Builder.Linear qualified as TB
+import Data.Type.Equality (pattern Refl)
 import Generics.SOP (
   ConstructorName,
   FieldName,
@@ -63,7 +65,7 @@ import Plutarch.Frontends.Data (
 import Plutarch.Frontends.LC (PPolymorphic)
 import Plutarch.Frontends.Nix (PNix)
 import Plutarch.Frontends.Untyped (PUntyped (punsafeCoerce))
-import Plutarch.PType (PCode, Pf' (Pf'), convertPfC)
+import Plutarch.PType (pHs_inverse, PCode, Pf' (Pf'))
 import Plutarch.Prelude
 import Plutarch.Repr.Newtype (PNewtyped (PNewtyped))
 import Plutarch.Repr.SOP (PSOPed (PSOPed))
@@ -75,6 +77,7 @@ data NixType
   = NFunTy NixType NixType
   | NTyLam NixType Text NixType
   | NForallTy NixType
+  | NSomeTy NixType
   | NTyVar Text
   | NSetTy [(Text, NixType)]
   | NAnyTy
@@ -116,6 +119,9 @@ serialiseTy' (NTyLam t v x) = do
 serialiseTy' (NForallTy x) = do
   x' <- serialiseTy' x
   pure $ "(forall " <> x' <> ")"
+serialiseTy' (NSomeTy x) = do
+  x' <- serialiseTy' x
+  pure $ "(some " <> x' <> ")"
 serialiseTy' NAnyTy = pure $ "Any"
 serialiseTy' NVoidTy = pure $ "Void"
 serialiseTy' (NUnionTy a b) = do
@@ -307,12 +313,21 @@ instance (IsPType (Impl m) a) => IsPTypePrim (Impl m) (PNewtyped a) where
 instance
   forall m a (f :: PHs a -> PType).
   IsPType (Impl m) ( 'PLam f :: PHs (a #-> PPType)) =>
-  IsPTypePrim (Impl m) (PForall f)
+  IsPTypePrim (Impl m) (PForall1 f)
   where
   isPTypePrim = IsPTypePrimData do
     body <- getTy (Proxy @m) (Proxy @( 'PLam f :: PHs (a #-> PPType)))
     pure $ NForallTy body
 
+instance
+  forall m a (f :: PHs a -> PType).
+  IsPType (Impl m) ( 'PLam f :: PHs (a #-> PPType)) =>
+  IsPTypePrim (Impl m) (PSome1 f)
+  where
+  isPTypePrim = IsPTypePrimData do
+    body <- getTy (Proxy @m) (Proxy @( 'PLam f :: PHs (a #-> PPType)))
+    pure $ NSomeTy body
+
 instance
   ( forall (x :: PHs a). IsPType (Impl m) x => IsPType (Impl m) (f x)
   , IsPType (Impl m) a
@@ -452,17 +467,49 @@ type family TyVar :: PHs a where
 instance
   forall m a (f :: PHs a -> PType).
   IsPType (Impl m) ( 'PLam f :: PHs (a #-> PPType)) =>
-  PConstructablePrim (Impl m) (PForall f)
+  PConstructablePrim (Impl m) (PForall1 f)
+  where
+  -- TODO: Add explicit big lambda at term-level? Otherwise you get weird comments
+  pconImpl t' = Impl do
+    lvl <- varify <$> getLvl
+    let d :: IsPTypeData (Impl m) (TyVar @a) = IsPTypeData $ IsPTypePrimData $ pure $ NTyVar lvl
+    withIsPType d $ case pHs_inverse @a of Refl -> do -- Why is GHC so ungodly stupid? Why the fuck do I need this much indentation?
+                                                      let PForall1 (t :: Term (Impl m) (f (TyVar @a))) = t'
+                                                      succLvl $ runTerm t
+  pmatchImpl t f = f (PForall1 (Term $ changeTy t))
+  pcaseImpl = error "FIXME"
+
+instance
+  forall m a (f :: PHs a -> PType).
+  IsPType (Impl m) ( 'PLam f :: PHs (a #-> PPType)) =>
+  PConstructablePrim (Impl m) (PSome1 f)
+  where
+  -- TODO: Add explicit big lambda at term-level? Otherwise you get weird comments
+  pconImpl t' = Impl case t' of
+      PSome1 (Proxy @x) t -> runTerm t
+  pmatchImpl t f = case pHs_inverse @a of
+    Refl -> Term $ Impl do
+      lvl <- varify <$> getLvl
+      let d :: IsPTypeData (Impl m) (TyVar @a) = IsPTypeData $ IsPTypePrimData $ pure $ NTyVar lvl
+      withIsPType d $ runTerm $ f (PSome1 (Proxy @(TyVar @a)) (Term $ changeTy t))
+  pcaseImpl = error "FIXME"
+
+{-
+instance
+  forall m a (f :: PHs a -> PType).
+  IsPType (Impl m) ( 'PLam f :: PHs (a #-> PPType)) =>
+  PConstructablePrim (Impl m) (PSome1 f)
   where
   -- TODO: Add explicit big lambda at term-level? Otherwise you get weird comments
   pconImpl t' = Impl do
     lvl <- varify <$> getLvl
     let d :: IsPTypeData (Impl m) (TyVar @a) = IsPTypeData $ IsPTypePrimData $ pure $ NTyVar lvl
-    withIsPType d $ convertPfC (Proxy @(IsPType (Impl m))) (Proxy @(TyVar @a)) do
-      let PForall (t :: Term (Impl m) (f (TyVar @a))) = t'
-      succLvl $ runTerm t
-  pmatchImpl t f = f (PForall (Term $ changeTy t))
+    withIsPType d $ case pHs_inverse @a of Refl -> do -- Why is GHC so ungodly stupid? Why the fuck do I need this much indentation?
+                                                      let PForall1 (t :: Term (Impl m) (f (TyVar @a))) = t'
+                                                      succLvl $ runTerm t
+  pmatchImpl t f = f (PForall1 (Term $ changeTy t))
   pcaseImpl = error "FIXME"
+-}
 
 instance PHasNewtypes (Impl m)
 instance Applicative m => PSOP (Impl m)

Plutarch/Frontends/Data.hs

@@ -11,8 +11,8 @@ module Plutarch.Frontends.Data (
   type (#=>) (..),
   type (#->) (..),
   PAny (..),
-  PForall (..),
-  PSome (..),
+  PForall1 (..),
+  PSome1 (..),
   PFix (..),
   PUnit (..),
   PPair (..),
@@ -21,6 +21,8 @@ module Plutarch.Frontends.Data (
   IsPTypeSOPData (..),
   PConstructorInfo (..),
   PRecursion,
+  type (#~)(PRefl),
+  PSingle,
 ) where
 
 import Data.Kind (Constraint, Type)
@@ -94,8 +96,8 @@ infixr 0 #->
 data PAny ef = forall a. PAny (Proxy a) (ef /$ a)
 instance PHasRepr PAny where type PReprSort _ = PReprPrimitive
 
-newtype PForall (f :: PHs a -> PType) ef = PForall (forall (forallvar :: PHs a). PfC ef forallvar => ef /$ f forallvar)
-instance PHasRepr (PForall ef) where type PReprSort _ = PReprPrimitive
+newtype PForall1 (f :: PHs a -> PType) ef = PForall1 (forall (forallvar :: PHs a). PfC ef forallvar => ef /$ f forallvar)
+instance PHasRepr (PForall1 ef) where type PReprSort _ = PReprPrimitive
 
 {-
 -- FIXME: uncomment this code when GHC has erased universal quantification
@@ -119,8 +121,8 @@ type PProxy' :: PHs (PTypeForall @PPType PProxyTypeF)
 type PProxy' = 'PTypeForall ('PProxyTypeF PProxy)
 -}
 
-data PSome (f :: PHs a -> PType) ef = forall (x :: PHs a). PSome (PfC ef x => ef /$ f x)
-instance PHasRepr (PSome ef) where type PReprSort _ = PReprPrimitive
+data PSome1 (f :: PHs a -> PType) ef = forall (x :: PHs a). PfC ef x => PSome1 (Proxy x) (ef /$ f x)
+instance PHasRepr (PSome1 ef) where type PReprSort _ = PReprPrimitive
 
 newtype PFix f ef = PFix (ef /$ f (PFix f))
 instance PHasRepr (PFix f) where type PReprSort _ = PReprPrimitive
@@ -134,6 +136,15 @@ instance PHasRepr (PPair a b) where type PReprSort _ = PReprPrimitive
 data PEither a b ef = PLeft (ef /$ a) | PRight (ef /$ b) deriving stock (Generic)
 instance PHasRepr (PEither a b) where type PReprSort _ = PReprPrimitive
 
+data (#~) (x :: PHs a) (y :: PHs a) ef where
+  PRefl :: (#~) x x ef
+instance PHasRepr (x #~ y) where type PReprSort _ = PReprPrimitive
+infix 4 #~
+
+type PSingle :: forall (a :: PType). PHs a -> PType
+data PSingle (x :: PHs a) ef
+instance PHasRepr (PSingle x) where type PReprSort _ = PReprPrimitive
+
 data PConstructorInfo ps :: Type where
   PConstructor :: PConstructorInfo ps
   PInfix :: PConstructorInfo '[a, b]

Plutarch/Frontends/LC.hs

@@ -6,7 +6,7 @@ module Plutarch.Frontends.LC (PLC, PPolymorphic) where
 
 import Data.Kind (Constraint)
 import Plutarch.Core (IsPType, IsPTypePrim, PConstructablePrim, PDSLKind)
-import Plutarch.Frontends.Data (PForall, type (#->) (PLam))
+import Plutarch.Frontends.Data (PForall1, PSome1, type (#->) (PLam))
 import Plutarch.PType (PHs, PPType, PType)
 
 class IsPTypePrim edsl x => IsPTypePrim' edsl x
@@ -19,7 +19,10 @@ type PPolymorphic :: PDSLKind -> Constraint
 class
   ( forall a (f :: PHs a -> PType).
     IsPType edsl ( 'PLam f :: PHs (a #-> PPType)) =>
-    PConstructablePrim edsl (PForall f)
+    PConstructablePrim edsl (PForall1 f)
+  , forall a (f :: PHs a -> PType).
+    IsPType edsl ( 'PLam f :: PHs (a #-> PPType)) =>
+    PConstructablePrim edsl (PSome1 f)
   , forall a b (f :: PHs a -> PHs b).
     (IsPType edsl a, IsPType edsl b, forall (x :: PHs a). IsPType edsl x => IsPType edsl (f x)) =>
     IsPTypePrim' edsl ( 'PLam f :: PHs (a #-> b))