use DimEq directly in typing context

lib/Quox/Typechecker.idr

@@ -62,13 +62,6 @@ subjMult : IsQty q => SQty q -> q -> SQty q
 subjMult sg pi = if isYes $ isZero pi then szero else sg
 
 
-export
-makeDimEq : DContext d -> DimEq d
-makeDimEq DNil           = zeroEq
-makeDimEq (DBind dctx)   = makeDimEq dctx :<? Nothing
-makeDimEq (DEq p q dctx) = set p q $ makeDimEq dctx
-
-
 parameters {auto _ : IsQty q} {auto _ : CanTC q m}
  mutual
   -- [todo] it seems like the options here for dealing with substitutions are
@@ -174,11 +167,10 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     (ty, l, r) <- expectEq !ask ty
     -- if Ψ, i | Γ ⊢ σ · t ⇐ A ⊳ Σ
     qout <- check (extendDim ctx) sg body.term ty.term
-    let eqs = makeDimEq ctx.dctx
     -- if Ψ | Γ ⊢ t‹0› = l : A‹0›
-    equal eqs ctx.tctx ty.zero body.zero l
+    equal ctx.dctx ctx.tctx ty.zero body.zero l
     -- if Ψ | Γ ⊢ t‹1› = r : A‹1›
-    equal eqs ctx.tctx ty.one body.one  r
+    equal ctx.dctx ctx.tctx ty.one body.one  r
     -- then Ψ | Γ ⊢ σ · (λᴰi ⇒ t) ⇐ Eq [i ⇒ A] l r ⊳ Σ
     pure qout
 
@@ -186,7 +178,7 @@ parameters {auto _ : IsQty q} {auto _ : CanTC q m}
     -- if Ψ | Γ ⊢ σ · e ⇒ A' ⊳ Σ
     infres <- infer ctx sg e
     -- if Ψ | Γ ⊢ A' <: A
-    subtype (makeDimEq ctx.dctx) ctx.tctx infres.type ty
+    subtype ctx.dctx ctx.tctx infres.type ty
     -- then Ψ | Γ ⊢ σ · e ⇐ A ⊳ Σ
     pure infres.qout