From d95a4f0983a6c278721d3da77050db1dec90616a Mon Sep 17 00:00:00 2001
From: Anupam Jain <ajnsit@gmail.com>
Date: Tue, 22 Oct 2024 14:29:56 +0530
Subject: [PATCH] Newtype some more to get reify working

---
 src/Singletons.purs | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/src/Singletons.purs b/src/Singletons.purs
index 206fae0..d63f6b9 100644
--- a/src/Singletons.purs
+++ b/src/Singletons.purs
@@ -2,7 +2,7 @@ module Singletons where
 
 import Control.Category (identity, (<<<))
 import Data.Exists (Exists, mkExists, runExists)
-import Data.Function (flip, (#))
+import Data.Function ((#))
 import Data.Leibniz (type (~), runLeibniz, symm)
 
 data Nat
@@ -32,9 +32,8 @@ reflect' = case _ of
   SSucc p -> p # runExists \ (Prev s _) -> Succ (reflect' s)
 
 -- Term -> Type
--- Why DOES this NOT work
--- reify :: forall r. (forall p. SNatOf p => r) -> Nat -> r
--- reify x n = runExists (withDNat x) (toSomeNat n)
+reify :: forall r. (forall p. Res p r) -> Nat -> r
+reify x n = runExists (withDNat x) (toSomeNat n)
 
 -- Isomorphic to Nat
 type SomeNat = Exists SNat
@@ -50,21 +49,25 @@ toSomeNat (Succ n) = toSomeNat n # runExists \sn -> mkExists (SSucc (mkExists (P
 ssucc :: SomeNat -> SomeNat
 ssucc = toSomeNat <<< Succ <<< fromSomeNat
 
-newtype DNat p = DNat (forall r. (SNatOf p => r) -> r)
+-- This is a newtype because - In a definition like this - `provideDNat x (DNat f) = f x`, where `f :: SNatOf p => r`
+--  the PS typchecker sees `f x` and elaborates `x` to take the `SNatOf` constraint even though it may not need it
+--  If we block off the constraint inside a newtype, it doesn't do this
+newtype Res p r = Res (SNatOf p => r)
+
+-- This is a newtype because runLeibniz needs it to be of the form `TypConstr p``
+-- And it doesn't seem to work well with type aliases
+newtype DNat p = DNat (forall r. Res p r -> r)
 
 captureDNat :: forall @p. SNatOf p => DNat p
-captureDNat = DNat \r -> r
+captureDNat = DNat \ (Res r) -> r
 
-provideDNat :: forall p r. (SNatOf p => r) -> DNat p -> r
-provideDNat = flip unDNat
-
-unDNat :: forall p r. DNat p -> (SNatOf p => r) -> r
+unDNat :: forall p r. DNat p -> Res p r -> r
 unDNat (DNat f) = f
 
 dNat :: forall p. SNat p -> DNat p
 dNat s = DNat (\x -> withDNat x s)
 
-withDNat :: forall p r. (SNatOf p => r) -> SNat p -> r
+withDNat :: forall p r. Res p r -> SNat p -> r
 withDNat x sn = case sn of
   SZero w -> unDNat (runLeibniz (symm w) (captureDNat @PZero)) x
   SSucc e -> e # runExists \ (Prev _ w) -> unDNat (runLeibniz (symm w) (dNat (runLeibniz w sn))) x