erasure improvements

newt/Prelude.newt

@@ -114,15 +114,16 @@ join mma = mma >>= id
 -- Equality
 
 infixl 1 _≡_
-data _≡_ : {A : U} -> A -> A -> U where
+data _≡_ : {0 A : U} -> A -> A -> U where
-  Refl :  {A : U} -> {a : A} -> a ≡ a
+  Refl :  {0 A : U} -> {a : A} -> a ≡ a
 
-replace : {A : U} {a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
+replace : {0 A : U} {0 a b : A} -> (P : A -> U) -> a ≡ b -> P a -> P b
 replace p Refl x = x
 
-cong : {A B : U} {a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
+cong : {0 A B : U} {0 a b : A} -> (f : A -> B) -> a ≡ b -> f a ≡ f b
+cong f Refl = Refl
 
-sym : {A : U} -> {a b : A} -> a ≡ b -> b ≡ a
+sym : {0 A : U} -> {0 a b : A} -> a ≡ b -> b ≡ a
 sym Refl = Refl
 
 
@@ -130,10 +131,10 @@ sym Refl = Refl
 -- Functor
 
 class Functor (m : U → U) where
-  map : {0 a b} → (a → b) → m a → m b
+  map : ∀ a b. (a → b) → m a → m b
 
 infixr 4 _<$>_ _<$_
-_<$>_ : {0 f} {{Functor f}} {0 a b} → (a → b) → f a → f b
+_<$>_ : ∀ f. {{Functor f}} {0 a b} → (a → b) → f a → f b
 f <$> ma = map f ma
 
 _<$_ : ∀ f a b. {{Functor f}} → b → f a → f b
@@ -167,8 +168,8 @@ instance Functor SnocList where
 infixl 3 _<*>_ _<*_ _*>_
 class Applicative (f : U → U) where
   -- appIsFunctor : Functor f
-  return : {0 a} → a → f a
+  return : ∀ a. a → f a
-  _<*>_ : {0 a b} -> f (a → b) → f a → f b
+  _<*>_ : ∀ a b. f (a → b) → f a → f b
 
 
 _<*_ : ∀ f a b. {{Applicative f}} → f a → f b → f a
@@ -188,10 +189,12 @@ instance Traversable List where
 traverse_ : ∀ t f a b. {{Traversable t}} {{Applicative f}} → (a → f b) → t a → f Unit
 traverse_ f xs = return (const MkUnit) <*> traverse f xs
 
-for : {t : U → U} {f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {a : U} → {b : U} → t a → (a → f b) → f (t b)
+-- FIXME - there is something subtly wrong in erasure here. t gets applied and there is no warning about it.
+-- maybe we don't check the head of an application?
+for : {0 t : U → U} {0 f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {0 a : U} → {0 b : U} → t a → (a → f b) → f (t b)
 for stuff fun = traverse fun stuff
 
-for_ : {t : U → U} {f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {a : U} → {b : U} → t a → (a → f b) → f Unit
+for_ : {0 t : U → U} {0 f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {0 a : U} → {0 b : U} → t a → (a → f b) → f Unit
 for_ stuff fun = return (const MkUnit) <*> traverse fun stuff
 
 instance Applicative Maybe where

port/Lib/Compile.newt

@@ -7,6 +7,7 @@ import Lib.Types
 import Lib.Prettier
 import Lib.CompileExp
 import Lib.TopContext
+import Lib.Erasure
 import Data.String
 import Data.Int
 import Data.SortedMap
@@ -282,7 +283,8 @@ maybeWrap stmt = Apply (JLam Nil stmt) Nil
 defToDoc : QName → Def → M Doc
 defToDoc name (Fn tm) = do
   debug $ \ _ => "compileFun \{render 90 $ pprint Nil tm}"
-  ct <- compileFun tm
+  tm' <- erase Nil tm Nil
+  ct <- compileFun tm'
   let exp = maybeWrap $ termToJS emptyJSEnv ct JReturn
   pure $ text "const" <+> jsIdent (show name) <+> text "=" <+/> expToDoc exp ++ text ";"
 defToDoc name Axiom = pure $ text ""

port/Lib/CompileExp.newt

@@ -73,11 +73,12 @@ compileTerm : Tm -> M CExp
 apply : CExp -> List CExp -> SnocList CExp -> Nat -> Tm -> M CExp
 -- out of args, make one up (fix that last arg)
 apply t Nil acc (S k) ty = pure $ CApp t (acc <>> Nil) (1 + cast k)
--- FIXME - this should be handled by Erasure.newt (wdiff of esbuild output says this is still used)
+-- FIXME - this should be handled by Erasure.newt
+-- We somehow hit the error below, with a Pi?
 apply t (x :: xs) acc (S k) (Pi y str icit Zero a b) =  apply t xs (acc :< CErased) k b
 apply t (x :: xs) acc (S k) (Pi y str icit Many a b) =  apply t xs (acc :< x) k b
 -- see if there is anything we have to handle here
-apply t (x :: xs) acc (S k) ty = error (getFC ty) "Expected pi \{showTm ty}. Overapplied function that escaped type checking?"
+apply t (x :: xs) acc (S k) ty = error (getFC ty) "Expected pi, got \{showTm ty}. Overapplied function that escaped type checking?"
 -- once we hit zero, we fold the rest
 apply t ts acc Z ty = go (CApp t (acc <>> Nil) 0) ts
   where
@@ -95,7 +96,7 @@ compileTerm t@(Ref fc nm) = do
           | Nothing => error fc "Undefined name \{show nm}"
   arity <- arityForName fc nm
   case arity of
-    -- we don't need tu curry functions that take one argument
+    -- we don't need to curry functions that take one argument
     (S Z) => pure $ CRef (show nm)
     _ => apply (CRef (show nm)) Nil Lin arity type
 
@@ -103,8 +104,9 @@ compileTerm (Meta _ k) = pure $ CRef "meta$\{show k}" -- FIXME
 compileTerm (Lam _ nm _ _ t) = CLam nm <$> compileTerm t
 compileTerm tm@(App _ _ _) = case funArgs tm of
   (Meta _ k, args) => do
-        info (getFC tm) "Compiling an unsolved meta \{show tm}"
+        error (getFC tm) "Compiling an unsolved meta \{show tm}"
-        pure $ CApp (CRef "Meta\{show k}") Nil 0
+        -- info (getFC tm) "Compiling an unsolved meta \{show tm}"
+        -- pure $ CApp (CRef "Meta\{show k}") Nil 0
   (t@(Ref fc nm), args) => do
         args' <- traverse compileTerm args
         arity <- arityForName fc nm

port/Lib/Erasure.newt

@@ -36,7 +36,9 @@ eraseSpine env t ((fc, arg) :: args) (Just (Pi fc1 str icit Many a b)) = do
   -- TODO this seems wrong, we need to subst u into b to get the type
   eraseSpine env (App fc t u) args (Just b)
 -- eraseSpine env t ((fc, arg) :: args) (Just ty) = do
---   error fc "ceci n'est pas une ∏ \{showTm ty}" -- e.g. Bnd 1
+--   -- Prelude Either and IO instance of <*> have Bnd here, possibly pattern matching
+--   -- unifying in the wrong direction? we should have something like a -> b
+--   error fc "ceci n'est pas une ∏ \{showTm ty} arg \{show arg}" -- e.g. Bnd 1
 eraseSpine env t ((fc, arg) :: args) _ = do
   u <- erase env arg Nil
   eraseSpine env (App fc t u) args Nothing

port/Lib/ProcessDecl.newt

@@ -162,12 +162,9 @@ processDecl ns (Def fc nm clauses) = do
   -- tm' <- nf Nil tm
   tm' <- zonk top 0 Nil tm
   debug $ \ _ => "NF\n\{render 80 $ pprint Nil tm'}"
-  -- TODO we want to keep both versions, but this is checking in addition to erasing
+  -- This is done in Compile.newt now, we can't store the result because we need the real thing at compile time
-  -- currently CompileExp is also doing erasure.
+  -- tm'' <- erase Nil tm' Nil
-  -- TODO we need erasure info on the lambdas or to fake up an appropriate environment
+  -- debug $ \ _ => "ERASED\n\{render 80 $ pprint Nil tm''}"
-  -- and erase inside. Currently the checking is imprecise
-  tm'' <- erase Nil tm' Nil
-  debug $ \ _ => "ERASED\n\{render 80 $ pprint Nil tm'}"
   debug $ \ _ => "Add def \{nm} \{render 90 $ pprint Nil tm'} : \{render 90 $ pprint Nil ty}"
   updateDef (QN ns nm) fc ty (Fn tm')
 

port/Lib/Types.newt

@@ -84,7 +84,7 @@ data Tm : U where
   -- need type?
   Let : FC -> Name -> Tm -> Tm -> Tm
   -- for desugaring where
-  LetRec : FC -> Name -> Tm -> Tm -> Tm -> Tm
+  LetRec : FC -> Name -> (ty : Tm) -> (t : Tm) -> (u : Tm) -> Tm
   Lit : FC -> Literal -> Tm
   Erased : FC -> Tm
 

port/Main.newt

@@ -18,7 +18,6 @@ import Lib.Tokenizer
 import Lib.TopContext
 import Lib.Types
 import Lib.Syntax
-import Lib.Syntax
 import Node
 import Serialize