factor out this case !mode of {..} stuff

lib/Quox/EffExtra.idr

@@ -27,6 +27,15 @@ local_ : Has (State s) fs => s -> Eff fs a -> Eff fs a
 local_ = localAt_ ()
 
 
+export %inline
+getsAt : (0 lbl : tag) -> Has (StateL lbl s) fs => (s -> a) -> Eff fs a
+getsAt lbl f = f <$> getAt lbl
+
+export %inline
+gets : Has (State s) fs => (s -> a) -> Eff fs a
+gets = getsAt ()
+
+
 export
 handleStateIORef : HasIO m => IORef st -> StateL lbl st a -> m a
 handleStateIORef r Get     = readIORef r

lib/Quox/Equal.idr

@@ -103,6 +103,11 @@ isSubSing defs ctx ty0 = do
     Box  {} => pure False
 
 
+private %inline
+bigger : Has EqModeState fs => (left, right : Lazy a) -> Eff fs a
+bigger l r = gets $ \case Super => l; _ => r
+
+
 export
 ensureTyCon : Has ErrorEff fs =>
               (loc : Loc) -> (ctx : EqContext n) -> (t : Term 0 n) ->
@@ -323,7 +328,7 @@ parameters (defs : Definitions)
       --    Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
       compareType (extendDim sTy.name Zero ctx) sTy.zero tTy.zero
       compareType (extendDim sTy.name One  ctx) sTy.one  tTy.one
-      let ty = case !mode of Super => sTy; _ => tTy
+      ty <- bigger sTy tTy
       local_ Equal $ do
         Term.compare0 ctx ty.zero sl tl
         Term.compare0 ctx ty.one  sr tr
@@ -493,8 +498,8 @@ parameters (defs : Definitions)
       --  Ψ | Γ ⊢ (s ∷ A) <: (t ∷ B) ⇒ B
       --
       -- and similar for :> and A
-      compare0' ctx (Ann s a _) (Ann t b _) _ _ =
+      compare0' ctx (Ann s a _) (Ann t b _) _ _ = do
-        let ty = case !mode of Super => a; _ => b in
+        ty <- bigger a b
         Term.compare0 ctx ty s t
 
       --  Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
@@ -509,7 +514,7 @@ parameters (defs : Definitions)
             ty1q = dsub1 ty1 q1; ty2q = dsub1 ty2 q2
         compareType ctx ty1p ty2p
         compareType ctx ty1q ty2q
-        let ty_p = case !mode of Super => ty1p; _ => ty2p
+        ty_p <- bigger ty1p ty2p
         Term.compare0 ctx ty_p val1 val2
       compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f