fix typing rules and (parts of) the typechecker

fixes rules for TyElim, TyLam, TyLet
move checkDef to inferDef
add a sigma to getPi
add rezz-scope to resurrect scopes from Γ

src/Context.agda

@@ -53,3 +53,10 @@ lookupVar (CtxExtend Γ y s) x p = raise (rezz _) (inBindCase p
   (λ q → lookupVar Γ x q))
 
 {-# COMPILE AGDA2HS lookupVar #-}
+
+rezz-scope : (Γ : Context α) → Rezz (Scope name) α
+rezz-scope CtxEmpty = rezz _
+rezz-scope (CtxExtend Γ x _) =
+  rezzCong (λ t → (singleton x) <> t) (rezz-scope Γ)
+
+{-# COMPILE AGDA2HS rezz-scope #-}

src/Conversion.agda

@@ -37,15 +37,18 @@ private variable
 data Conv (@0 Γ : Context α) : @0 Type α → @0 Term α → @0 Term α → Set
 data ConvElim (@0 Γ : Context α) : @0 Type α → @0 Term α → @0 Elim α → @0 Elim α → Set
 
-@0 renameTop : Term (x ◃ α) → Term (y ◃ α)
-renameTop {x = x} {y = y} = substTerm (liftBindSubst {x = x} {y = y} (idSubst (rezz _)))
+renameTop : Rezz _ α → Term (x ◃ α) → Term (y ◃ α)
+renameTop {x = x} {y = y} r = substTerm (liftBindSubst {x = x} {y = y} (idSubst r))
+
+@0 renameTopE : Term (x ◃ α) → Term (y ◃ α)
+renameTopE = renameTop (rezz _)
 
 data Conv {α} Γ where
   CRefl  : Conv Γ t u u
-  CLam   : Conv {α = x ◃ α} (Γ , x ∶ a) b (renameTop u) (renameTop v)
+  CLam   : Conv {α = x ◃ α} (Γ , x ∶ a) b (renameTopE u) (renameTopE v)
          → Conv Γ (TPi x k l a b) (TLam y u) (TLam z v)
   CPi    : Conv Γ (TSort k) a a'
-         → Conv (Γ , x ∶ a) (TSort (weakenSort (subWeaken subRefl) l)) b (renameTop b')
+         → Conv (Γ , x ∶ a) (TSort (weakenSort (subWeaken subRefl) l)) b (renameTopE b')
          → Conv Γ (TSort (funSort k l)) (TPi x k l a b) (TPi y k l a' b')
   CApp   : Conv Γ a u u'
          → ConvElim Γ a u w w'

src/Typechecker.agda

@@ -74,7 +74,17 @@ postulate
   liftMaybe : Maybe a → TCError → TCM a
   liftEither : Either TCError a → TCM a
 
-
+-- this is Either and not TCM because otherwise some meta doesn't get solved 🤷
+getPi : (t : Term α)
+      → Either TCError
+               (Σ0 (name)
+                   (λ x → ∃ ((Sort α × Sort α) × (Type α × Type (x ◃ α)))
+                             (λ ( (sa , sb) , (ta , tb) ) → t ≡ TPi x sa sb ta tb)
+                    ))
+getPi term@(TPi x sa sr at rt) = Right ( ⟨ x ⟩ ((sa , sr) , (at , rt)) ⟨ refl ⟩)
+getPi _ = Left "coudn't reduce the term to become a pi type"
+
+{-# TERMINATING #-}
 inferType : (te : Term α)
           → TCM (∃ (Type α) (λ ty → Γ ⊢ te ∷ ty))
 
@@ -90,25 +100,22 @@ inferApp : (u : Term α)
            (e : Elim α)
            → TCM (∃ (Type α) (λ ty → Γ ⊢ TApp u e ∷ ty))
 inferApp {α = α} {Γ = Γ} u (Syntax.EArg v) = do
+  let r = (rezz-scope Γ)
   (tu ⟨ gtu ⟩ ) ← inferType {Γ = Γ} u
   fuel <- tcmFuel
   pifuel <- liftMaybe
               (tryFuel stepEither (Left (makeState tu)) fuel)
               "couldn't construct Fuel for Pi reduction"
-  -- FIXME: need to resurrect α, can be done from Γ potentially?            
-  let rpi = reduce (rezz _) tu pifuel
-  (⟨ x ⟩ ( (sv , sr) , (tv , tr))) ← liftEither (getPi rpi)
+  let rpi = reduce r tu pifuel
+  --Would be nice to have an inlined case here instead of getPi
+  --https://agda.readthedocs.io/en/latest/language/syntactic-sugar.html#do-notation
+  --but it won't get compiled to haskell
+  (⟨ x ⟩ ((sv , sr) , (tv , tr)) ⟨ eq ⟩) ← liftEither (getPi rpi)
+  --FIXME: this should be CRedL, but that requires eq to be matched with refl
+  --atm agda can't unify it
   let gc = convert {Γ = Γ} (TSort (funSort sv sr)) tu (TPi x sv sr tv tr)
   gtv ← checkType {Γ = Γ} v tv
-  -- FIXME: need to resurrect α, can be done from Γ potentially?            
-  return ((substTop (rezz _) v tr) ⟨ TyAppE gtu (TyArg gc gtv) ⟩ )
-  where
-    getPi : Term α
-          → Either TCError
-                   (Σ0 (name)
-                       (λ x → (Sort α × Sort α) × (Type α × Type (x ◃ α))))
-    getPi term@(TPi x sa sr at rt) = Right ( ⟨ x ⟩ ((sa , sr) , (at , rt)))
-    getPi _ = Left "coudn't reduce the term to become a pi type"
+  return ((substTop r v tr) ⟨ TyAppE gtu (TyArg gc gtv) ⟩ )
 inferApp {Γ = Γ} u (Syntax.EProj x x₁) = tcError "not implemented"
 inferApp {Γ = Γ} u (Syntax.ECase bs) = tcError "not implemented"
 
@@ -126,25 +133,19 @@ inferTySort : (s : Sort α)
             → TCM (∃ (Type α) (λ ty → Γ ⊢ TSort s ∷ ty))
 inferTySort (STyp x) = return (TSort (STyp (suc x)) ⟨ TyType ⟩)
 
-checkDef : (@0 f : name)
+inferDef : (@0 f : name)
            (p : f ∈ defs)
-           (ty : Type α)
-           → TCM (Γ ⊢ TDef f p ∷ ty)
-checkDef f p ty = do
-  -- FIXME: doesn't work with the error: weaken subEmpty (lookupAll defType p) != ty
-  --return (TyDef f)
-  tcError "can't typecheck because idk how"
+         → TCM (∃ (Type α) (λ ty → Γ ⊢ TDef f p ∷ ty))
+inferDef f p = return (((weaken subEmpty (defType ! f))) ⟨ (TyDef f) ⟩)
 
 checkLambda : (@0 x : name)
               (u : Term (x ◃ α))
               (ty : Type α)
               → TCM (Γ ⊢ TLam x u ∷ ty)
 checkLambda {Γ = Γ} x u (TPi y su sv tu tv) = do
-  -- FIXME: the names x and y don't match
-  --d ← checkType {Γ = Γ , x ∶ tu} u tv
-  --return (TyLam d)
-  tcError "can't typecheck because idk how"
---FIXME
+  d ← checkType {Γ = Γ , y ∶ tu} (renameTop (rezz-scope Γ) u) tv
+  return (TyLam d)
+--FIXME: reduce ty and see if it's a Pi
 checkLambda x u _ = tcError "can't check lambda against a type that isn't a Pi"
 
 checkLet : (@0 x : name)
@@ -155,9 +156,7 @@ checkLet : (@0 x : name)
 checkLet {Γ = Γ} x u v ty = do
   tu ⟨ dtu ⟩  ← inferType {Γ = Γ} u
   dtv ← checkType {Γ = Γ , x ∶ tu} v (weaken (subWeaken subRefl) ty)
-  -- FIXME: doesn't work with the error: substTop (rezz α) u ty != ty
-  --return (TyLet dtu dtv)
-  tcError "can't typecheck because idk how"
+  return (TyLet {r = rezz-scope Γ} dtu dtv)
 
 checkConv : (t : Term α)
             (cty tty : Type α)
@@ -169,7 +168,10 @@ checkType {Γ = Γ} t@(TVar x p) ty = do
   tvar ← inferVar {Γ = Γ} x p
   (tsor ⟨ _ ⟩) ← inferSort {Γ = Γ} ty
   checkConv {Γ = Γ} t ty (TSort tsor) tvar
-checkType (TDef f p) ty = checkDef f p ty
+checkType {Γ = Γ} (TDef d p) ty =  do
+  tdef ← inferDef d p
+  (tsor ⟨ _ ⟩) ← inferSort {Γ = Γ} ty
+  checkConv {Γ = Γ} (TDef d p) ty (TSort tsor) tdef
 checkType (TCon c p x) ty = tcError "not implemented yet"
 checkType (TLam x te) ty =  checkLambda x te ty
 checkType {Γ = Γ} t@(TApp u e) ty = do
@@ -188,7 +190,7 @@ checkType (TLet x u v) ty = checkLet x u v ty
 checkType (TAnn u t) ty = tcError "not implemented yet"
 
 inferType (TVar x p) = inferVar x p
-inferType (TDef d x) = tcError "can't infer the type of a definition"
+inferType (TDef d p) = inferDef d p
 inferType (TCon c p x) = tcError "not implemented yet"
 inferType (TLam x te) = tcError "can't infer the type of a lambda"
 inferType (TApp u e) = inferApp u e

src/Typing.agda

@@ -64,10 +64,10 @@ data TyTerm {α} Γ where
     -- TODO: constructor typing
 
     TyLam :
-
-         (Γ , x ∶ s) ⊢ u ∷ t
+          {@0 r : Rezz _ α}
+         →  (Γ , x ∶ s) ⊢ (renameTop r u) ∷ t
        ------------------------------------------------------------
-       →  Γ            ⊢ TLam x u ∷ TPi x k l s t
+       →  Γ            ⊢ TLam y u ∷ TPi x k l s t
 
     TyAppE :
           Γ ⊢ u ∷ s
@@ -87,12 +87,12 @@ data TyTerm {α} Γ where
         --------------------------------------------
          Γ ⊢ TSort (STyp n) ∷ TSort (STyp (suc n))
 
-    TyLet :
+    TyLet : {r : Rezz _ α}
 
-           Γ           ⊢ u ∷ s
-         → (Γ , x ∶ s) ⊢ v ∷ t
+         → Γ           ⊢ u ∷ s
+         → (Γ , x ∶ s) ⊢ v ∷ (weaken (subWeaken subRefl) t)
          ------------------------------------------
-         → Γ ⊢ TLet x u v ∷ substTop (rezz α) u t
+         → Γ ⊢ TLet x u v ∷ t
 
     TyAnn :
             Γ ⊢ u ∷ t
@@ -108,11 +108,11 @@ data TyTerm {α} Γ where
 
 {-# COMPILE AGDA2HS TyTerm #-}
 
-data TyElim Γ where
-    TyArg :
-          Conv Γ (TSort k) v (TPi x l m s t)
+data TyElim {α} Γ where
+    TyArg : {@0 r : Rezz _ α}
+        → Conv Γ (TSort k) v (TPi x l m s t)
         → TyTerm Γ u s
-        → TyElim Γ (EArg u) v (λ h → substTop (rezz _) u t)
+        → TyElim Γ (EArg u) v (λ h → substTop r u t)
     -- TODO: proj
     -- TODO: case