From 0e3a9fe605f00ad0b4179a31129bdb116d816431 Mon Sep 17 00:00:00 2001
From: Steve Dunham <dunhamsteve@gmail.com>
Date: Sat, 21 Sep 2024 15:44:51 -0700
Subject: [PATCH] notes on typeclass

---
 TODO.md             |  2 +-
 newt/typeclass.newt | 41 +++++++++--------------------------------
 src/Lib/Check.idr   |  4 ++++
 src/Lib/TT.idr      |  2 +-
 src/Lib/Types.idr   | 11 ++++++-----
 5 files changed, 21 insertions(+), 39 deletions(-)

diff --git a/TODO.md b/TODO.md
index aa18faf..ecfe60d 100644
--- a/TODO.md
+++ b/TODO.md
@@ -20,7 +20,7 @@ I may be done with `U` - I keep typing `Type`.
   - Agda doesn't have it, clashes with pair syntax
 - [ ] import
 - [ ] autos / typeclass resolution
-  - Can we solve right away when creating the implicit, or do we need postpone?
+  - We need special handling in unification to make this possible
   - options
     - keep as implicit and do auto if the type constructor is flagged auto
     - keep as implicit and mark auto, behavior overlaps a lot with implicit
diff --git a/newt/typeclass.newt b/newt/typeclass.newt
index 35f5855..bfedee9 100644
--- a/newt/typeclass.newt
+++ b/newt/typeclass.newt
@@ -15,9 +15,6 @@ data Maybe : U -> U where
   Nothing : {A : U} -> Maybe A
 
 
--- NEXT trying to get this to work. An equivalence is not found in pattern
--- matching
-
 -- [instance]
 MaybeMonad : Monad Maybe
 -- Agda case lambda might be nice..
@@ -29,43 +26,23 @@ MaybeMonad = MkMonad {Maybe} (\ {A} ma amb =>
       -- oh, but var 0 value is var5
       Just a => amb a)
 
--- so if we added {{ }} and search...
--- second arg will be {{}}
--- add implicit patterns first
+-- So the idea here is to have some implicits that are solved by search
 
--- I need a way to tag `x : Monad m` as auto.  I could do {{}}, but maybe I should tag the `data` for search?
--- It should be a record, but I don't have records yet
+_>>=_ : {a b : U} -> {m : U -> U} -> {x : Monad m} -> (m a) -> (a -> m b) -> m b
+_>>=_ {a} {b} {m} {MkMonad bind'}  ma amb = bind' {a} {b} ma amb
 
-bind : {m : U -> U} -> {x : Monad m} -> {a b : U} -> (m a) -> (a -> m b) -> m b
-bind {m} {MkMonad bind'} = bind'
+infixl 1 _>>=_
 
 ptype Int
 
 -- For now, we may try to solve this at creation time, but it's possible postpone is needed
 
-/-
+-- *SOLVE meta 6 sp [< (%var 0 [< ]), (%meta 4 [< (%var 0 [< ])])] val (%ref Maybe [< (%meta 9 [< (%var 0 [< ]), (%var 1 [< ])])])
 
-So I think we need to solve meta 7 first, and then if we're lucky, it's var 0 and we're
-good to go.
+-- Essentially   (m6 v0) (m4 ...) == Maybe Int and (m6 v0) (m2 v0) == Maybe Int
 
-  foo x = bind {_} {_} {_} (Just x) (\ x => Just x)
-  failed to unify ( Maybe ( ?m:10 x:0 ) )
-    with ( ( ?m:4 x:0 ) ( ?m:8 x:0 ) )
-  non-variable in pattern (%meta 8 [< (%var 0 [< ])])
-
-  If I stick Int in third slot:
-  foo x = bind {_} {_} {Int} (Just x) (\ x => Just x)
-                                    ^
-  failed to unify ( Maybe ( ?m:8 x:0 ) )
-    with ( ( ?m:4 x:0 ) Int )
-  non-variable in pattern (%ref Int [< ])
-
-  -- If I slot in MaybeMonad, all is happy.
-  foo x = bind {_} {MaybeMonad} {_} (Just x) (\ x => Just x)
-
-  -- And a maybe up front has only the auto unsolved.
-
--/
+-- Idris gets this by specially treating determining arguments of an auto as "invertible". It then unifies
+-- the last arg on each side and tries the rest, which is now in the pattern fragment.
 
 foo : Int -> Maybe Int
-foo x = bind {Maybe} {_} {_} (Just x) (\ x => Just x)
+foo x = _>>=_ (Just x) (\ x  => Just 10)
diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr
index 809987b..fbc8e25 100644
--- a/src/Lib/Check.idr
+++ b/src/Lib/Check.idr
@@ -102,6 +102,9 @@ parameters (ctx: Context)
 
   solve : Nat -> Nat -> SnocList Val -> Val  -> M  ()
   solve l m sp t = do
+    debug "solve \{show l} \{show m} \{show sp} \{show t}"
+    meta <- lookupMeta m
+    debug "meta \{show meta}"
     ren <- invert l sp
     tm <- rename m ren l t
     let tm = lams (length sp) tm
@@ -156,6 +159,7 @@ parameters (ctx: Context)
       (VLam fc _ t,  t'       ) => unify (l + 1) !(t $$ VVar emptyFC l [<]) !(t' `vapp` VVar emptyFC l [<])
       (VMeta fc k sp,  VMeta fc' k' sp' ) =>
         if k == k' then unifySpine l (k == k') sp sp'
+        -- TODO, might want to try the other way, too.
         else solve l k sp (VMeta fc' k' sp') >> pure neutral
       (t,           VMeta fc' i' sp') => solve l i' sp' t >> pure neutral
       (VMeta fc i sp, t'           ) => solve l i sp t' >> pure neutral
diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr
index af15b34..a12a781 100644
--- a/src/Lib/TT.idr
+++ b/src/Lib/TT.idr
@@ -37,7 +37,7 @@ export
 freshMeta : Context -> FC -> Val -> M Tm
 freshMeta ctx fc ty = do
   mc <- readIORef ctx.metas
-  putStrLn "INFO at \{show fc}: fresh meta \{show mc.next}"
+  putStrLn "INFO at \{show fc}: fresh meta \{show mc.next} : \{show ty}"
   writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty ::) } mc
   pure $ applyBDs 0 (Meta emptyFC mc.next) ctx.bds
   where
diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr
index 371414a..d6751f0 100644
--- a/src/Lib/Types.idr
+++ b/src/Lib/Types.idr
@@ -292,11 +292,6 @@ record Context
 public export
 data MetaEntry = Unsolved FC Nat Context Val | Solved Nat Val
 
-export
-covering
-Show MetaEntry where
-  show (Unsolved pos k xs ty) = "Unsolved \{show pos} \{show k} : \{show ty}"
-  show (Solved k x) = "Solved \{show k} \{show x}"
 
 public export
 record MetaContext where
@@ -366,6 +361,12 @@ record Context where
   metas : IORef MetaContext
   fc : FC
 
+export
+covering
+Show MetaEntry where
+  show (Unsolved pos k ctx ty) = "Unsolved \{show pos} \{show k} : \{show ty} \{show ctx.bds}"
+  show (Solved k x) = "Solved \{show k} \{show x}"
+
 export withPos : Context -> FC -> Context
 withPos ctx fc = { fc := fc } ctx