fix erasure issues inside where clauses (add type to LetRec)

TODO.md

@@ -1,7 +1,7 @@
 
 ## TODO
 
-- [ ] SortedMap.newt issue in `where`
+- [x] SortedMap.newt issue in `where`
 - [x] fix "insufficient patterns", wire in M or Either String
 - [ ] Matching _,_ when Maybe is expected should be an error
 - [ ] error for repeated names on LHS
@@ -18,7 +18,7 @@
 - [ ] literals for double
 - [ ] add default failing case for constructor matching to catch errors
 - [x] Add icit to Lam (see `check` for details)
-  - [ ] make change to `check`
+  - [ ] make change to `check` NOW
 - [ ] add jump to definition magic to vscode extension
 - [ ] TCO? Probably needed in browser, since v8 doesn't do it. bun and JavaScriptCore do support it.
 - [x] deconstructing `let` (and do arrows)

aoc2024/SortedMap.newt

@@ -57,19 +57,11 @@ updateMap k v (MapOf map) = case insertT23 k v map of
   Left map' => MapOf map'
   Right (a, b, c) => MapOf (Node2 a b c)
 
--- FIXME this doesn't work in a `where` because Letrec doesn't have the type
-toList' : ∀ k v h. T23 h k v → List (k × v) → List (k × v)
-toList' (Leaf k v) acc = (k, v) :: acc
-toList' (Node2 t1 k1 t2) acc = toList' t2 (toList' t1 acc)
-toList' (Node3 t1 k1 t2 k2 t3) acc = toList' t3 $ toList' t2 $ toList' t1 acc
-
 toList : ∀ k v. SortedMap k v → List (k × v)
-toList {k} {v} (MapOf smap) = reverse $ toList' smap Nil
+toList {k} {v} (MapOf smap) = reverse $ go smap Nil
-  -- FIXME erasure checking false positive (need type on foo in env when processing Letrec)
+  where
-  -- where
+    go : ∀ h. T23 h k v → List (k × v) → List (k × v)
-  --   foo : ∀ k v h. T23 h k v → List (k × v) → List (k × v)
+    go (Leaf k v) acc = (k, v) :: acc
-  --   foo (Leaf k v) acc = (k, v) :: acc
+    go (Node2 t1 k1 t2) acc = go t2 (go t1 acc)
-  --   foo (Node2 t1 k1 t2) acc = foo t2 (foo t1 acc)
+    go (Node3 t1 k1 t2 k2 t3) acc = go t3 $ go t2 $ go t1 acc
-  --   foo (Node3 t1 k1 t2 k2 t3) acc = foo t3 $ foo t2 $ foo t1 acc
 toList _ = Nil
-

src/Lib/Compile.idr

@@ -328,7 +328,7 @@ process (done,docs) nm = do
     walkTm (App x t u) acc = walkTm t !(walkTm u acc)
     walkTm (Pi x str icit y t u) acc = walkTm t !(walkTm u acc)
     walkTm (Let x str t u) acc = walkTm t !(walkTm u acc)
-    walkTm (LetRec x str t u) acc = walkTm t !(walkTm u acc)
+    walkTm (LetRec x str _ t u) acc = walkTm t !(walkTm u acc)
     walkTm (Case x t alts) acc = foldlM walkAlt acc alts
     walkTm _ acc = pure acc
 

src/Lib/CompileExp.idr

@@ -143,7 +143,7 @@ compileTerm (Case _ t alts) = do
   pure $ CCase t' alts'
 compileTerm (Lit _ lit) = pure $ CLit lit
 compileTerm (Let _ nm t u) = pure $ CLet nm !(compileTerm t) !(compileTerm u)
-compileTerm (LetRec _ nm t u) = pure $ CLetRec nm !(compileTerm t) !(compileTerm u)
+compileTerm (LetRec _ nm _ t u) = pure $ CLetRec nm !(compileTerm t) !(compileTerm u)
 compileTerm (Erased _) = pure CErased
 
 export

src/Lib/Elab.idr

@@ -181,8 +181,9 @@ rename meta ren lvl v = go ren lvl v
     go ren lvl (VLit fc lit) = pure (Lit fc lit)
     go ren lvl (VLet fc name val body) =
       pure $ Let fc name !(go ren lvl val) !(go (lvl :: ren) (S lvl) body)
-    go ren lvl (VLetRec fc name val body) =
+    -- these probably shouldn't show up in solutions...
-      pure $ Let fc name !(go (lvl :: ren) (S lvl) val) !(go (lvl :: ren) (S lvl) body)
+    go ren lvl (VLetRec fc name ty val body) =
+      pure $ LetRec fc name !(go ren lvl ty) !(go (lvl :: ren) (S lvl) val) !(go (lvl :: ren) (S lvl) body)
 
 lams : Nat -> List String -> Tm -> Tm
 lams 0 _ tm = tm
@@ -731,7 +732,7 @@ checkWhere ctx decls body ty = do
   -- Should we run the rest with the definition in place?
   -- I'm wondering if switching from bind to define will mess with metas
   -- let ctx' = define ctx name vtm vty
-  pure $ LetRec sigFC name tm !(checkWhere ctx' decls' body ty)
+  pure $ LetRec sigFC name funTy tm !(checkWhere ctx' decls' body ty)
 
 
 checkDone : Context -> List (String, Pattern) -> Raw -> Val -> M Tm

src/Lib/Erasure.idr

@@ -77,10 +77,10 @@ erase env t sp = case t of
     u' <- erase env u []
     v' <- erase ((nm, Many, Nothing) :: env) v []
     eraseSpine env (Let fc nm u' v') sp Nothing
-  (LetRec fc nm u v) => do
+  (LetRec fc nm ty u v) => do
-    u' <- erase ((nm, Many, Nothing) :: env) u []
+    u' <- erase ((nm, Many, Just ty) :: env) u []
-    v' <- erase ((nm, Many, Nothing) :: env) v []
+    v' <- erase ((nm, Many, Just ty) :: env) v []
-    eraseSpine env (LetRec fc nm u' v') sp Nothing
+    eraseSpine env (LetRec fc nm ty u' v') sp Nothing
   (Bnd fc k) => do
     case getAt k env of
       Nothing => error fc "bad index \{show k}"

src/Lib/Eval.idr

@@ -153,7 +153,7 @@ eval env mode (Meta fc i) =
 eval env mode (Lam fc x icit rig t) = pure $ VLam fc x icit rig (MkClosure env t)
 eval env mode (Pi fc x icit rig a b) = pure $ VPi fc x icit rig !(eval env mode a) (MkClosure env b)
 eval env mode (Let fc nm t u) = pure $ VLet fc nm !(eval env mode t) !(eval (VVar fc (length env) [<] :: env) mode u)
-eval env mode (LetRec fc nm t u) = pure $ VLetRec fc nm !(eval (VVar fc (length env) [<] :: env) mode t) !(eval (VVar fc (length env) [<] :: env) mode u)
+eval env mode (LetRec fc nm ty t u) = pure $ VLetRec fc nm !(eval env mode ty) !(eval (VVar fc (length env) [<] :: env) mode t) !(eval (VVar fc (length env) [<] :: env) mode u)
 -- Here, we assume env has everything. We push levels onto it during type checking.
 -- I think we could pass in an l and assume everything outside env is free and
 -- translate to a level
@@ -189,7 +189,7 @@ quote l (VMeta fc i sp) =
 quote l (VLam fc x icit rig t) = pure $ Lam fc x icit rig !(quote (S l) !(t $$ VVar emptyFC l [<]))
 quote l (VPi fc x icit rig a b) = pure $ Pi fc x icit rig !(quote l a) !(quote (S l) !(b $$ VVar emptyFC l [<]))
 quote l (VLet fc nm t u) = pure $ Let fc nm !(quote l t) !(quote (S l) u)
-quote l (VLetRec fc nm t u) = pure $ LetRec fc nm !(quote (S l) t) !(quote (S l) u)
+quote l (VLetRec fc nm ty t u) = pure $ LetRec fc nm !(quote l ty) !(quote (S l) t) !(quote (S l) u)
 quote l (VU fc) = pure (U fc)
 quote l (VRef fc n def sp) = quoteSp l (Ref fc n def) sp
 quote l (VCase fc sc alts) = pure $ Case fc !(quote l sc) alts
@@ -249,7 +249,7 @@ tweakFC fc (App fc1 t u) = App fc t u
 tweakFC fc (Pi fc1 nm icit x t u) = Pi fc nm icit x t u
 tweakFC fc (Case fc1 t xs) = Case fc t xs
 tweakFC fc (Let fc1 nm t u) = Let fc nm t u
-tweakFC fc (LetRec fc1 nm t u) = LetRec fc nm t u
+tweakFC fc (LetRec fc1 nm ty t u) = LetRec fc nm ty t u
 tweakFC fc (Lit fc1 lit) = Lit fc lit
 tweakFC fc (Erased fc1) = Erased fc
 
@@ -282,7 +282,7 @@ zonk top l env t = case t of
   (App fc t u) => zonkApp top l env t [!(zonk top l env u)]
   (Pi fc nm icit rig a b) => Pi fc nm icit rig <$> zonk top l env a <*> zonkBind top l env b
   (Let fc nm t u) => Let fc nm <$> zonk top l env t <*> zonkBind top l env u
-  (LetRec fc nm t u) => LetRec fc nm <$> zonkBind top l env t <*> zonkBind top l env u
+  (LetRec fc nm ty t u) => LetRec fc nm <$> zonk top l env ty <*> zonkBind top l env t <*> zonkBind top l env u
   (Case fc sc alts) => Case fc <$> zonk top l env sc <*> traverse (zonkAlt top l env) alts
   U fc => pure $ U fc
   Lit fc lit => pure $ Lit fc lit

src/Lib/Types.idr

@@ -125,7 +125,7 @@ data Tm : Type where
   -- need type?
   Let : FC -> Name -> Tm -> Tm -> Tm
   -- for desugaring where
-  LetRec : FC -> Name -> Tm -> Tm -> Tm
+  LetRec : FC -> Name -> Tm -> Tm -> Tm -> Tm
   Lit : FC -> Literal -> Tm
   Erased : FC -> Tm
 
@@ -143,7 +143,7 @@ HasFC Tm where
   getFC (Case fc t xs) = fc
   getFC (Lit fc _) = fc
   getFC (Let fc _ _ _) = fc
-  getFC (LetRec fc _ _ _) = fc
+  getFC (LetRec fc _ _ _ _) = fc
   getFC (Erased fc) = fc
 
 covering
@@ -169,7 +169,7 @@ Show Tm where
   show (Pi _ str Auto rig t u) = "(Pi {{\{show rig}\{str} : \{show t}}} => \{show u})"
   show (Case _ sc alts) = "(Case \{show sc} \{show alts})"
   show (Let _ nm t u) = "(Let \{nm} \{show t} \{show u})"
-  show (LetRec _ nm t u) = "(LetRec \{nm} \{show t} \{show u})"
+  show (LetRec _ nm ty t u) = "(LetRec \{nm} : \{show ty} \{show t} \{show u})"
   show (Erased _) = "ERASED"
 
 public export
@@ -244,7 +244,7 @@ pprint names tm = go 0 names tm
     go p names (Case _ sc alts) = parens 0 p $ text "case" <+> go 0 names sc <+> text "of" ++ (nest 2 (line ++ stack (map (goAlt 0 names) alts)))
     go p names (Lit _ lit) = text (show lit)
     go p names (Let _ nm t u) = parens 0 p $ text "let" <+> text nm <+> ":=" <+> go 0 names t <+> "in" </> (nest 2 $ go 0 (nm :: names) u)
-    go p names (LetRec _ nm t u) = parens 0 p $ text "letrec" <+> text nm <+> ":=" <+> go 0 names t <+> "in" </> (nest 2 $ go 0 (nm :: names) u)
+    go p names (LetRec _ nm ty t u) = parens 0 p $ text "letrec" <+> text nm <+> ":" <+> go 0 names ty <+> ":=" <+> go 0 names t <+> "in" </> (nest 2 $ go 0 (nm :: names) u)
     go p names (Erased _) = "ERASED"
 data Val : Type
 
@@ -277,7 +277,7 @@ data Val : Type where
   VLam : FC -> Name -> Icit -> Quant -> Closure -> Val
   VPi : FC -> Name -> Icit -> Quant -> (a : Lazy Val) -> (b : Closure) -> Val
   VLet : FC -> Name -> Val -> Val -> Val
-  VLetRec : FC -> Name -> Val -> Val -> Val
+  VLetRec : FC -> Name -> Val -> Val -> Val -> Val
   VU : FC -> Val
   VErased : FC -> Val
   VLit : FC -> Literal -> Val
@@ -294,7 +294,7 @@ getValFC (VU fc) = fc
 getValFC (VErased fc) = fc
 getValFC (VLit fc _) = fc
 getValFC (VLet fc _ _ _) = fc
-getValFC (VLetRec fc _ _ _) = fc
+getValFC (VLetRec fc _ _ _ _) = fc
 
 
 public export
@@ -316,7 +316,7 @@ Show Val where
   show (VU _) = "U"
   show (VLit _ lit) = show lit
   show (VLet _ nm a b) = "(%let \{show nm} = \{show a} in \{show b}"
-  show (VLetRec _ nm a b) = "(%letrec \{show nm} = \{show a} in \{show b}"
+  show (VLetRec _ nm ty a b) = "(%letrec \{show nm} : \{show ty} = \{show a} in \{show b}"
   show (VErased _) = "ERASED"
 
 public export