examples/bool.quox

@@ -1,34 +1,35 @@
-load "misc.quox";
+load "misc.quox"
 
 namespace bool {
 
-def0 Bool : ★ = {true, false};
+def0 Bool : ★ = {true, false}
 
 def if-dep : 0.(P : Bool → ★) → (b : Bool) → ω.(P 'true) → ω.(P 'false) → P b =
-  λ P b t f ⇒ case b return b' ⇒ P b' of { 'true ⇒ t; 'false ⇒ f };
+  λ P b t f ⇒ case b return b' ⇒ P b' of { 'true ⇒ t; 'false ⇒ f }
 
-def if : 0.(A : ★) → (b : Bool) → ω.A → ω.A → A =
+def if : 0.(A : ★) → Bool → ω.A → ω.A → A =
-  λ A ⇒ if-dep (λ _ ⇒ A);
+  λ A ⇒ if-dep (λ _ ⇒ A)
 
 def0 if-same : (A : ★) → (b : Bool) → (x : A) → if A b x x ≡ x : A =
-  λ A b x ⇒ if-dep (λ b' ⇒ if A b' x x ≡ x : A) b (δ _ ⇒ x) (δ _ ⇒ x);
+  λ A b x ⇒ if-dep (λ b' ⇒ if A b' x x ≡ x : A) b (δ _ ⇒ x) (δ _ ⇒ x)
 
 def if2 : 0.(A B : ★) → (b : Bool) → ω.A → ω.B → if¹ ★ b A B =
-  λ A B ⇒ if-dep (λ b ⇒ if-dep¹ (λ _ ⇒ ★) b A B);
+  λ A B ⇒ if-dep (λ b ⇒ if¹ ★ b A B)
 
-def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False;
+def0 T : Bool → ★ = λ b ⇒ if¹ ★ b True False
 
-def boolω : Bool → [ω.Bool] =
+def dup : Bool → [ω.Bool] =
-  λ b ⇒ if [ω.Bool] b ['true] ['false];
+  λ b ⇒ if [ω.Bool] b ['true] ['false]
 
-def true-not-false : Not ('true ≡ 'false : Bool) =
+def0 true-not-false : Not ('true ≡ 'false : Bool) =
-  λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true;
+  λ eq ⇒ coe (𝑖 ⇒ T (eq @𝑖)) 'true
 
 
 -- [todo] infix
-def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false;
+def and : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a b 'false
-def or  : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b;
+def or  : Bool → ω.Bool → Bool = λ a b ⇒ if Bool a 'true b
 
 }
 
-def0 Bool = bool.Bool;
+def0 Bool = bool.Bool
+def if = bool.if

examples/natw.quox

@@ -0,0 +1,36 @@
+load "misc.quox"
+
+namespace natw {
+
+def0 Tag : ★ = {z, s}
+
+def0 Child : Tag → ★ =
+  λ t ⇒ case t return ★ of { 'z ⇒ {}; 's ⇒ {pred} }
+
+def0 NatW : ★ = (t : Tag) ⊲ Child t
+
+def Zero : NatW =
+  'z ⋄ (λ v ⇒ case v return NatW of {})
+
+def Suc : ω.NatW → NatW =
+  λ n ⇒ 's ⋄ (λ u ⇒ case u return NatW of { 'pred ⇒ n })
+
+def elim : 0.(P : NatW → ★) →
+           ω.(P Zero) →
+           ω.(0.(n : NatW) → ω.(P n) → P (Suc n)) →
+           ω.(n : NatW) → P n =
+  λ P pz ps n ⇒
+  caseω n return n' ⇒ P n' of {
+    t ⋄ f, ω.ih ⇒
+      (case t
+       return t' ⇒ 0.(eq : t ≡ t' : Tag) →
+         P (t' ⋄ coe (𝑖 ⇒ ω.(Child (eq @𝑖)) → NatW) f)
+       of {
+         'z ⇒ λ _ ⇒ pz;
+         's ⇒ λ eq ⇒
+           ps (f  (coe (𝑖 ⇒ Child (eq @𝑖)) @1 @0 'pred))
+              (ih (coe (𝑖 ⇒ Child (eq @𝑖)) @1 @0 'pred))
+       }) (δ 𝑖 ⇒ t)
+  }
+
+}

lib/Quox/Displace.idr

@@ -19,6 +19,9 @@ parameters (k : Universe)
     doDisplace (Lam body loc) = Lam (doDisplaceS body) loc
     doDisplace (Sig fst snd loc) = Sig (doDisplace fst) (doDisplaceS snd) loc
     doDisplace (Pair fst snd loc) = Pair (doDisplace fst) (doDisplace snd) loc
+    doDisplace (W shape body loc) =
+      W (doDisplace shape) (doDisplaceS body) loc
+    doDisplace (Sup root sub loc) = Sup (doDisplace root) (doDisplace sub) loc
     doDisplace (Enum cases loc) = Enum cases loc
     doDisplace (Tag tag loc) = Tag tag loc
     doDisplace (Eq ty l r loc) =
@@ -47,6 +50,8 @@ parameters (k : Universe)
     doDisplace (App fun arg loc) = App (doDisplace fun) (doDisplace arg) loc
     doDisplace (CasePair qty pair ret body loc) =
       CasePair qty (doDisplace pair) (doDisplaceS ret) (doDisplaceS body) loc
+    doDisplace (CaseW qty qtyIH tree ret body loc) =
+      CaseW qty qtyIH (doDisplace tree) (doDisplaceS ret) (doDisplaceS body) loc
     doDisplace (CaseEnum qty tag ret arms loc) =
       CaseEnum qty (doDisplace tag) (doDisplaceS ret) (map doDisplace arms) loc
     doDisplace (CaseNat qty qtyIH nat ret zero succ loc) =

lib/Quox/EffExtra.idr

@@ -26,6 +26,26 @@ local_ : Has (State s) fs => s -> Eff fs a -> Eff fs a
 local_ = localAt_ ()
 
 
+public export
+record StateRes s a where
+  constructor SR
+  state  : s
+  result : a
+
+export
+stateAt : (0 lbl : tag) -> Has (StateL lbl s) fs =>
+          (s -> StateRes s a) -> Eff fs a
+stateAt lbl f = do
+  s <- getAt lbl
+  let out = f s
+  putAt lbl out.state
+  pure out.result
+
+export %inline
+state : Has (State s) fs => (s -> StateRes s a) -> Eff fs a
+state = stateAt ()
+
+
 export
 hasDrop : (0 neq : Not (a = b)) ->
           (ha : Has a fs) => (hb : Has b fs) =>

lib/Quox/Equal.idr

@@ -79,6 +79,8 @@ sameTyCon (Pi   {}) (Pi   {}) = True
 sameTyCon (Pi   {}) _         = False
 sameTyCon (Sig  {}) (Sig  {}) = True
 sameTyCon (Sig  {}) _         = False
+sameTyCon (W    {}) (W    {}) = True
+sameTyCon (W    {}) _         = False
 sameTyCon (Enum {}) (Enum {}) = True
 sameTyCon (Enum {}) _         = False
 sameTyCon (Eq   {}) (Eq   {}) = True
@@ -111,6 +113,7 @@ isSubSing defs ctx ty0 = do
     Sig {fst, snd, _} =>
       isSubSing defs ctx fst `andM`
       isSubSing defs (extendTy Zero snd.name fst ctx) snd.term
+    W {} => pure False
     Enum {cases, _} =>
       pure $ length (SortedSet.toList cases) <= 1
     Eq {} => pure True
@@ -120,6 +123,7 @@ isSubSing defs ctx ty0 = do
     E _ => pure False
     Lam  {} => pure False
     Pair {} => pure False
+    Sup  {} => pure False
     Tag  {} => pure False
     DLam {} => pure False
     Zero {} => pure False
@@ -211,7 +215,7 @@ parameters (defs : Definitions)
           -- --------------------------------------------
           --    Γ ⊢ (s₁, t₁) = (s₂, t₂) : (x : A) × B
           --
-          -- [todo] η for π ≥ 0 maybe
+          -- [todo] η for π ≰ 1 maybe
           (Pair sFst sSnd {}, Pair tFst tSnd {}) => do
             compare0 ctx fst sFst tFst
             compare0 ctx (sub1 snd (Ann sFst fst fst.loc)) sSnd tSnd
@@ -225,6 +229,27 @@ parameters (defs : Definitions)
           (E _,     t) => wrongType t.loc ctx ty t
           (s,       _) => wrongType s.loc ctx ty s
 
+      compare0' ctx ty@(W {shape, body, _}) s t =
+        case (s, t) of
+          --           Γ ⊢ s₁ = t₁ : A
+          --  Γ ⊢ s₂ = t₂ : ω.B[s₁∷A/x] → (x : A) ⊲ B
+          -- -----------------------------------------
+          --     Γ ⊢ s₁⋄s₂ = t₁⋄t₂ : (x : A) ⊲ B
+          (Sup sRoot sSub {}, Sup tRoot tSub {}) => do
+            compare0 ctx shape sRoot tRoot
+            let arg   = sub1 body (Ann sRoot shape sRoot.loc)
+                subTy = Arr Any arg ty ty.loc
+            compare0 ctx subTy sSub tSub
+
+          (E e, E f) => Elim.compare0 ctx e f
+
+          (Sup {}, E   {}) => clashT s.loc ctx ty s t
+          (E   {}, Sup {}) => clashT s.loc ctx ty s t
+
+          (Sup {}, t) => wrongType t.loc ctx ty t
+          (E   {}, t) => wrongType t.loc ctx ty t
+          (s,      _) => wrongType s.loc ctx ty s
+
       compare0' ctx ty@(Enum {}) s t = local_ Equal $
         case (s, t) of
           -- --------------------
@@ -322,12 +347,16 @@ parameters (defs : Definitions)
       --  Γ ⊢ Type 𝓀 <: Type ℓ
       expectModeU a.loc !mode k l
 
-    compareType' ctx a@(Pi {qty = sQty, arg = sArg, res = sRes, _})
+    compareType' ctx (Pi {qty = sQty, arg = sArg, res = sRes, loc})
                      (Pi {qty = tQty, arg = tArg, res = tRes, _}) = do
       --   Γ ⊢ A₁ :> A₂    Γ, x : A₁ ⊢ B₁ <: B₂
       -- ----------------------------------------
-      --  Γ ⊢ (π·x : A₁) → B₁ <: (π·x : A₂) → B₂
+      --  Γ ⊢ π.(x : A₁) → B₁ <: π.(x : A₂) → B₂
-      expectEqualQ a.loc sQty tQty
+      --
+      -- no quantity subtyping since that would need a runtime coercion
+      -- e.g. if ⌊0.A → B⌋ ⇝ ⌊B⌋, then the promotion to ω.A → B would need
+      -- to re-add the abstraction
+      expectEqualQ loc sQty tQty
       local flip $ compareType ctx sArg tArg -- contra
       compareType (extendTy Zero sRes.name sArg ctx) sRes.term tRes.term
 
@@ -339,12 +368,20 @@ parameters (defs : Definitions)
       compareType ctx sFst tFst
       compareType (extendTy Zero sSnd.name sFst ctx) sSnd.term tSnd.term
 
+    compareType' ctx (W {shape = sShape, body = sBody, loc})
+                     (W {shape = tShape, body = tBody, _}) = do
+      --  Γ ⊢ A₁ <: A₂    Γ, x : A₁ ⊢ B₁ <: B₂
+      -- --------------------------------------
+      --   Γ ⊢ (x : A₁) ⊲ B₁ <: (x : A₂) ⊲ B₂
+      compareType ctx sShape tShape
+      compareType (extendTy Zero sBody.name sShape ctx) sBody.term tBody.term
+
     compareType' ctx (Eq {ty = sTy, l = sl, r = sr, _})
                      (Eq {ty = tTy, l = tl, r = tr, _}) = do
       --            Γ ⊢ A₁‹ε/i› <: A₂‹ε/i›
-      --  Γ ⊢ l₁ = l₂ : A₁‹𝟎/i›    Γ ⊢ r₁ = r₂ : A₁‹𝟏/i›
+      --  Γ ⊢ l₁ = l₂ : A₁‹0/i›    Γ ⊢ r₁ = r₂ : A₁‹1/i›
       -- ------------------------------------------------
-      --    Γ ⊢ Eq [i ⇒ A₁] l₁ r₂ <: Eq [i ⇒ A₂] l₂ r₂
+      --    Γ ⊢ 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
@@ -366,6 +403,9 @@ parameters (defs : Definitions)
       pure ()
 
     compareType' ctx (BOX pi a loc) (BOX rh b {}) = do
+      --     Γ ⊢ A <: B
+      -- --------------------
+      --  Γ ⊢ [π.A] <: [π.B]
       expectEqualQ loc pi rh
       compareType ctx a b
 
@@ -439,6 +479,36 @@ parameters (defs : Definitions)
           expectEqualQ e.loc epi fpi
       compare0' ctx e@(CasePair {}) f _ _ = clashE e.loc ctx e f
 
+      --  Ψ | Γ ⊢ e = f ⇒ (x : A) ⊲ B
+      --  Ψ | Γ, p : (x : A) ⊲ B ⊢ Q = R ⇐ Type
+      --  Ψ | Γ, x : A, y : ω.B → (x : A) ⊲ B, ih : 1.(z : B) → Q[y z/p]
+      --    ⊢ s = t ⇐ Q[(x⋄y ∷ (x : A) ⊲ B)/p]
+      -- ----------------------------------------------------------------
+      --  Ψ | Γ ⊢ caseπ e return Q of { x ⋄ y, ς.ih ⇒ s }
+      --        = caseπ f return R of { x ⋄ y, ς.ih ⇒ t } ⇒ Q[e/p]
+      compare0' ctx (CaseW epi epi' e eret ebody eloc)
+                    (CaseW fpi fpi' f fret fbody floc) ne nf =
+        local_ Equal $ do
+          compare0 ctx e f
+          ety <- computeElimTypeE defs ctx e @{noOr1 ne}
+          compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
+          (shape, tbody) <- expectW defs ctx eloc ety
+          let [< x, y, ih] = ebody.names
+          z <- mnb "z" ih.loc
+          let xbind = (epi, x, shape)
+              ybind = (epi, y, Arr Any tbody.term (weakT 1 ety) y.loc)
+              ihbind = (epi', ih,
+                PiY One z
+                  (sub1 (weakS 2 tbody) (BV 1 x.loc))
+                  (sub1 (weakS 3 eret) (App (BV 1 y.loc) (BVT 0 z.loc) ih.loc))
+                  ih.loc)
+              ctx' = extendTyN [< xbind, ybind, ihbind] ctx
+          Term.compare0 ctx' (substCaseWRet ebody.names ety eret)
+            ebody.term fbody.term
+          expectEqualQ e.loc epi  fpi
+          expectEqualQ e.loc epi' fpi'
+      compare0' ctx e@(CaseW {}) f _ _ = clashE e.loc ctx e f
+
       --  Ψ | Γ ⊢ e = f ⇒ {𝐚s}
       --  Ψ | Γ, x : {𝐚s} ⊢ Q = R
       --  Ψ | Γ ⊢ sᵢ = tᵢ ⇐ Q[𝐚ᵢ∷{𝐚s}]
@@ -451,10 +521,13 @@ parameters (defs : Definitions)
           compare0 ctx e f
           ety <- computeElimTypeE defs ctx e @{noOr1 ne}
           compareType (extendTy Zero eret.name ety ctx) eret.term fret.term
-          for_ !(expectEnum defs ctx eloc ety) $ \t => do
+          for_ (SortedMap.toList earms) $ \(t, l) => do
-            l <- lookupArm eloc t earms
             r <- lookupArm floc t farms
             compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r
+          -- for_ !(expectEnum defs ctx eloc ety) $ \t => do
+          --   l <- lookupArm eloc t earms
+          --   r <- lookupArm floc t farms
+          --   compare0 ctx (sub1 eret $ Ann (Tag t l.loc) ety l.loc) l r
           expectEqualQ eloc epi fpi
         where
           lookupArm : Loc -> TagVal -> CaseEnumArms d n -> Equal_ (Term d n)
@@ -522,16 +595,18 @@ parameters (defs : Definitions)
 
       --  Ψ | Γ ⊢ A‹p₁/𝑖› <: B‹p₂/𝑖›
       --  Ψ | Γ ⊢ A‹q₁/𝑖› <: B‹q₂/𝑖›
-      --  Ψ | Γ ⊢ e <: f ⇒ _
+      --  Ψ | Γ ⊢ s <: t ⇐ B‹p₂/𝑖›
-      --    (non-neutral forms have the coercion already pushed in)
       -- -----------------------------------------------------------
-      --  Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ e
+      --  Ψ | Γ ⊢ coe [𝑖 ⇒ A] @p₁ @q₁ s
-      --       <: coe [𝑖 ⇒ B] @p₂ @q₂ f ⇒ B‹q₂/𝑖›
+      --       <: coe [𝑖 ⇒ B] @p₂ @q₂ t ⇒ B‹q₂/𝑖›
-      compare0' ctx (Coe ty1 p1 q1 (E val1) _)
+      compare0' ctx (Coe ty1 p1 q1 val1 _)
-                    (Coe ty2 p2 q2 (E val2) _) ne nf = do
+                    (Coe ty2 p2 q2 val2 _) ne nf = do
-        compareType ctx (dsub1 ty1 p1) (dsub1 ty2 p2)
+        let typ1 = dsub1 ty1 p1; tyq1 = dsub1 ty1 q1
-        compareType ctx (dsub1 ty1 q1) (dsub1 ty2 q2)
+            typ2 = dsub1 ty2 p2; tyq2 = dsub1 ty2 q2
-        compare0 ctx val1 val2
+        compareType ctx typ1 typ2
+        compareType ctx tyq1 tyq2
+        let ty = case !mode of Super => typ1; _ => typ2
+        Term.compare0 ctx ty val1 val2
       compare0' ctx e@(Coe {}) f _ _ = clashE e.loc ctx e f
 
       -- (no neutral compositions in a closed dctx)
@@ -598,6 +673,13 @@ parameters (defs : Definitions)
                  (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
         compare0 ctx (weakT 2 ret) b1.term b2.term
 
+      compareArm_ ctx KW ret u b1 b2 = do
+        let [< a, b] = b1.names
+            ctx = extendTyN
+              [< (Zero, a, TYPE u a.loc),
+                 (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)] ctx
+        compare0 ctx (weakT 2 ret) b1.term b2.term
+
       compareArm_ ctx KEnum ret u b1 b2 =
         compare0 ctx ret b1.term b2.term
 

lib/Quox/Loc.idr

@@ -109,10 +109,16 @@ or (L l1) (L l2) = L $ l1 `or_` l2
 public export
 interface Located a where (.loc) : a -> Loc
 
+export %inline Located Loc where l.loc = l
+
 public export
 0 Located1 : (a -> Type) -> Type
 Located1 f = forall x. Located (f x)
 
+public export
+0 Located2 : (a -> b -> Type) -> Type
+Located2 f = forall x, y. Located (f x y)
+
 public export
 interface Located a => Relocatable a where setLoc : Loc -> a -> a
 

lib/Quox/Name.idr

@@ -4,7 +4,7 @@ import Quox.Loc
 import Quox.CharExtra
 import public Data.SnocList
 import Data.List
-import Control.Eff
+import Quox.EffExtra
 import Text.Lexer
 import Derive.Prelude
 
@@ -178,23 +178,22 @@ export
 runNameGen : Has NameGen fs => Eff fs a -> Eff (fs - NameGen) a
 runNameGen = map fst . runNameGenWith 0
 
+export
+gen : Has NameGen fs => Eff fs Nat
+gen = stateAt GEN $ \i => SR {result = i, state = S i}
+
 ||| generate a fresh name with the given base
 export
 mn : Has NameGen fs => PBaseName -> Eff fs BaseName
-mn base = do
+mn base = MN base <$> gen
-  i <- getAt GEN
-  modifyAt GEN S
-  pure $ MN base i
 
-||| generate a fresh binding name with the given base and
+||| generate a fresh binding name with the given base and location `loc`
-||| (optionally) location `loc`
 export
-mnb : Has NameGen fs =>
+mnb : Has NameGen fs => PBaseName -> Loc -> Eff fs BindName
-      PBaseName -> {default noLoc loc : Loc} -> Eff fs BindName
+mnb base loc = pure $ BN !(mn base) loc
-mnb base = pure $ BN !(mn base) loc
 
 export
 fresh : Has NameGen fs => BindName -> Eff fs BindName
-fresh (BN (UN str)   loc) = mnb str {loc}
+fresh (BN (UN str)   loc) = mnb str loc
-fresh (BN (MN str k) loc) = mnb str {loc}
+fresh (BN (MN str k) loc) = mnb str loc
-fresh (BN Unused     loc) = mnb "x" {loc}
+fresh (BN Unused     loc) = mnb "x" loc

lib/Quox/No.idr

@@ -52,3 +52,18 @@ export %inline
 nchoose : (b : Bool) -> Either (So b) (No b)
 nchoose True  = Left  Oh
 nchoose False = Right Ah
+
+
+private
+0 notFalseTrue : (a : Bool) -> not a = True -> a = False
+notFalseTrue False Refl = Refl
+
+export %inline
+soNot : So (not a) -> No a
+soNot x with 0 (not a) proof eq
+  soNot Oh | True =
+    rewrite notFalseTrue a eq in Ah
+
+export %inline
+soNot' : So a -> No (not a)
+soNot' Oh = Ah

lib/Quox/Parser/FromParser.idr

@@ -150,6 +150,23 @@ mutual
     Pair s t loc =>
       Pair <$> fromPTermWith ds ns s <*> fromPTermWith ds ns t <*> pure loc
 
+    W x s t loc =>
+      W <$> fromPTermWith ds ns s
+        <*> fromPTermTScope ds ns [< x] t
+        <*> pure loc
+
+    Sup s t loc =>
+      Sup <$> fromPTermWith ds ns s
+          <*> fromPTermWith ds ns t
+          <*> pure loc
+
+    Case pi tree (r, ret) (CaseW x y (rh, ih) body _) loc =>
+      map E $ CaseW (fromPQty pi) (fromPQty rh)
+        <$> fromPTermElim ds ns tree
+        <*> fromPTermTScope ds ns [< r] ret
+        <*> fromPTermTScope ds ns [< x, y, ih] body
+        <*> pure loc
+
     Case pi pair (r, ret) (CasePair (x, y) body _) loc =>
       map E $ CasePair (fromPQty pi)
         <$> fromPTermElim ds ns pair
@@ -157,13 +174,6 @@ mutual
         <*> fromPTermTScope ds ns [< x, y] body
         <*> pure loc
 
-    Case pi tag (r, ret) (CaseEnum arms _) loc =>
-      map E $ CaseEnum (fromPQty pi)
-        <$> fromPTermElim ds ns tag
-        <*> fromPTermTScope ds ns [< r] ret
-        <*> assert_total fromPTermEnumArms ds ns arms
-        <*> pure loc
-
     Nat loc => pure $ Nat loc
     Zero loc => pure $ Zero loc
     Succ n loc => [|Succ (fromPTermWith ds ns n) (pure loc)|]
@@ -185,6 +195,13 @@ mutual
 
     Tag str loc => pure $ Tag str loc
 
+    Case pi tag (r, ret) (CaseEnum arms _) loc =>
+      map E $ CaseEnum (fromPQty pi)
+        <$> fromPTermElim ds ns tag
+        <*> fromPTermTScope ds ns [< r] ret
+        <*> assert_total fromPTermEnumArms ds ns arms
+        <*> pure loc
+
     Eq (i, ty) s t loc =>
       Eq <$> fromPTermDScope ds ns [< i] ty
          <*> fromPTermWith ds ns s

lib/Quox/Parser/Lexer.idr

@@ -197,6 +197,8 @@ reserved =
    Sym "×" `Or` Sym "**",
    Sym "≡" `Or` Sym "==",
    Sym "∷" `Or` Sym "::",
+   Sym "⊲" `Or` Sym "<|",
+   Sym "⋄" `Or` Sym "<>",
    Punc1 '.',
    Word1 "case",
    Word1 "case0", Word1 "case1",

lib/Quox/Parser/Parser.idr

@@ -212,7 +212,8 @@ export
 qtyPatVar : FileName -> Grammar True (PQty, PatVar)
 qtyPatVar fname =
       [|(,) (qty fname) (needRes "." *> patVar fname)|]
-  <|> [|(,) (defLoc fname $ PQ One) (patVar fname)|]
+  <|> do name <- patVar fname
+         pure (PQ (if isUnused name then Zero else One) name.loc, name)
 
 
 export
@@ -226,6 +227,7 @@ data PCasePat =
   | PZero Loc
   | PSucc PatVar PQty PatVar Loc
   | PBox  PatVar Loc
+  | PSup  PatVar PatVar PQty PatVar Loc
 %runElab derive "PCasePat" [Eq, Ord, Show]
 
 export
@@ -235,6 +237,7 @@ Located PCasePat where
   (PZero         loc).loc = loc
   (PSucc _ _ _   loc).loc = loc
   (PBox  _       loc).loc = loc
+  (PSup  _ _ _ _ loc).loc = loc
 
 ||| either `zero` or `0`
 export
@@ -251,6 +254,11 @@ casePat fname = withLoc fname $
          ih <- resC "," *> qtyPatVar fname
            <|> [|(,) (defLoc fname $ PQ Zero) (unused fname)|]
          pure $ PSucc p (fst ih) (snd ih)
+  <|> do x <- patVar fname
+         y <- resC "⋄" *> patVar fname
+         ih <- resC "," *> qtyPatVar fname
+           <|> [|(,) (defLoc fname $ PQ Zero) (unused fname)|]
+         pure $ PSup x y (fst ih) (snd ih)
   <|> delim "[" "]" [|PBox (patVar fname)|]
   <|> fatalError "invalid pattern"
 
@@ -405,12 +413,19 @@ appTerm fname =
   <|> succTerm fname
   <|> normalAppTerm fname
 
+export
+supTerm : FileName -> Grammar True PTerm
+supTerm fname = withLoc fname $ do
+  l <- appTerm fname; commit
+  r <- optional $ res "⋄" *> assert_total supTerm fname
+  pure $ \loc => maybe l (\r => Sup l r loc) r
+
 export
 infixEqTerm : FileName -> Grammar True PTerm
 infixEqTerm fname = withLoc fname $ do
-  l <- appTerm fname; commit
+  l <- supTerm fname; commit
   rest <- optional $ res "≡" *>
-    [|(,) (assert_total term fname) (needRes ":" *> appTerm fname)|]
+    [|(,) (assert_total term fname) (needRes ":" *> supTerm fname)|]
   let u = Unused $ onlyStart l.loc
   pure $ \loc => maybe l (\rest => Eq (u, snd rest) l (fst rest) loc) rest
 
@@ -430,8 +445,38 @@ lamTerm fname = withLoc fname $ do
     body <- assert_total term fname; commit
     pure $ \loc => foldr (\x, s => k x s loc) body xs
 
+
+private
+data BindType = BPi | BW | BSig
+%runElab derive "BindType" [Eq, Ord]
+
+private
+data BindSequence' b a = BLast a | BMore a b (BindSequence' b a)
+
+private
+data BindTypeL = BTL BindType Loc
+%runElab derive "BindTypeL" [Eq, Ord]
+
+private
+data BindPart = BT (Maybe PQty) (List1 PatVar) PTerm
+Located BindPart where
+  (BT q xs t).loc = maybe (head xs).loc (.loc) q `extendL` t.loc
+
+
+private
+BindSequence : Type
+BindSequence = BindSequence' BindTypeL BindPart
+
+private
+bindType : FileName -> Grammar True BindTypeL
+bindType fname = bt BPi "→" <|> bt BW "⊲" <|> bt BSig "×"
+where
+  bt : BindType -> (s : String) -> (0 _ : IsReserved s) =>
+       Grammar True BindTypeL
+  bt t str = withLoc fname $ resC str $> BTL t
+
 -- [todo] fix the backtracking in e.g. (F x y z × B)
-export
+private
 properBinders : FileName -> Grammar True (List1 PatVar, PTerm)
 properBinders fname = assert_total $ do
   -- putting assert_total directly on `term`, in this one function,
@@ -441,61 +486,85 @@ properBinders fname = assert_total $ do
   t  <- term fname;          needRes ")"
   pure (xs, t)
 
-export
+private
-sigmaTerm : FileName -> Grammar True PTerm
+bindPart : FileName -> Grammar True BindPart
-sigmaTerm fname =
+bindPart fname = do
-      (properBinders fname >>= continueDep)
+  qty <- optional $ qty fname <* resC "."
-  <|> (annTerm fname       >>= continueNondep)
+  bnd <- properBinders fname
-where
+     <|> do n <- unused fname
-  continueDep : (List1 PatVar, PTerm) -> Grammar True PTerm
+            t <- if isJust qty then termArg fname else annTerm fname
-  continueDep (names, fst) = withLoc fname $ do
+            pure (singleton n, t)
-    snd <- needRes "×" *> sigmaTerm fname
+  pure $ uncurry (BT qty) bnd
-    pure $ \loc => foldr (\x, snd => Sig x fst snd loc) snd names
 
-  cross : PTerm -> PTerm -> PTerm
+private
-  cross l r = let loc = extend' l.loc r.loc.bounds in
+bindSequence : FileName -> Grammar True BindSequence
-              Sig (Unused $ onlyStart l.loc) l r loc
+bindSequence fname = do
+  x  <- bindPart fname
+  by <- optional $ do
+    b <- bindType fname
+    y <- mustWork $ assert_total bindSequence fname
+    pure (b, y)
+  pure $ maybe (BLast x) (\by => BMore x (fst by) (snd by)) by
 
-  continueNondep : PTerm -> Grammar False PTerm
+private
-  continueNondep fst = do
+fromBindSequence : BindSequence -> Grammar False PTerm
-    rest <- optional $ resC "×" *> sepBy1 (res "×") (annTerm fname)
+fromBindSequence as = go [<] as where
-    pure $ foldr1 cross $ fst ::: maybe [] toList rest
+  -- the ol’ shunty
+  data Elem = E BindPart BindTypeL
+
+  fatalLoc' : Located z => z -> String -> Grammar False a
+  fatalLoc' z = maybe fatalError fatalLoc z.loc.bounds
+
+  toTerm : BindPart -> Grammar False PTerm
+  toTerm (BT Nothing (Unused _ ::: []) s) = pure s
+  toTerm s = fatalLoc' s $
+    "binder with no following body\n" ++
+    "(maybe some missing parens)"
+
+  fromTerm : PTerm -> BindPart
+  fromTerm t = BT Nothing (singleton $ Unused t.loc) t
+
+  checkNoQty : String -> Maybe PQty -> Grammar False ()
+  checkNoQty s (Just q) = fatalLoc' q "no quantity allowed with \{s}"
+  checkNoQty _ _ = pure ()
+
+  apply : Elem -> PTerm -> Grammar False PTerm
+  apply (E s'@(BT mqty xs s) (BTL b _)) t = case b of
+    BPi => do
+      let q   = fromMaybe (PQ One s.loc) mqty
+          loc = s'.loc `extendL` t.loc
+      pure $ foldr (\x, t => Pi q x s t loc) t xs
+    BW => do
+      checkNoQty "⊲" mqty
+      when (length xs /= 1) $ do
+        let loc = foldr1 extendL $ map (.loc) xs
+        fatalLoc' loc "only one binding allowed with ⊲"
+      pure $ W (head xs) s t (s.loc `extendL` t.loc)
+    BSig => do
+      checkNoQty "×" mqty
+      let loc = s'.loc `extendL` t.loc
+      pure $ foldr (\x, t => Sig x s t loc) t xs
+
+  end : SnocList Elem -> PTerm -> Grammar False PTerm
+  end [<]       t = pure t
+  end (es :< e) t = end es !(apply e t)
+
+  go : SnocList Elem -> BindSequence -> Grammar False PTerm
+  go es (BLast a) = do
+    end es !(toTerm a)
+  go [<] (BMore a b as) =
+    go [< E a b] as
+  go (es :< e@(E a' b')) (BMore a b as) =
+    if b' > b then do
+      t <- apply e !(toTerm a)
+      go (es :< E (fromTerm t) b) as
+    else
+      go (es :< e :< E a b) as
 
 export
-piTerm : FileName -> Grammar True PTerm
+bindTerm : FileName -> Grammar True PTerm
-piTerm fname = withLoc fname $ do
+bindTerm fname = fromBindSequence !(bindSequence fname)
-  q   <- [|GivenQ $ qty fname <* resC "."|] <|> defLoc fname DefaultQ
-  dom <- [|Dep $ properBinders fname|] <|> [|Nondep $ ndDom q fname|]
-  cod <- optional $ do resC "→"; assert_total term fname <* commit
-  when (needCod q dom && isNothing cod) $ fail "missing function type result"
-  pure $ maybe (const $ toTerm dom) (makePi q dom) cod
-where
-  data PiQty = GivenQ PQty | DefaultQ Loc
-  data PiDom = Dep (List1 PatVar, PTerm) | Nondep PTerm
 
-  ndDom : PiQty -> FileName -> Grammar True PTerm
-  ndDom (GivenQ   _) = termArg   -- ｢1.(List A)｣, not ｢1.List A｣
-  ndDom (DefaultQ _) = sigmaTerm
-
-  needCod : PiQty -> PiDom -> Bool
-  needCod (DefaultQ _) (Nondep _) = False
-  needCod _            _          = True
-
-  toTerm : PiDom -> PTerm
-  toTerm (Dep (_, s)) = s
-  toTerm (Nondep s)   = s
-
-  toQty : PiQty -> PQty
-  toQty (GivenQ   qty) = qty
-  toQty (DefaultQ loc) = PQ One loc
-
-  toDoms : PQty -> PiDom -> List1 (PQty, PatVar, PTerm)
-  toDoms qty (Dep (xs, s)) = [(qty, x, s) | x <- xs]
-  toDoms qty (Nondep s)    = singleton (qty, Unused s.loc, s)
-
-  makePi : PiQty -> PiDom -> PTerm -> Loc -> PTerm
-  makePi q doms cod loc =
-    foldr (\(q, x, s), t => Pi q x s t loc) cod $ toDoms (toQty q) doms
 
 public export
 PCaseArm : Type
@@ -529,6 +598,9 @@ checkCaseArms loc ((PSucc p q ih _, rhs1) :: rest) = do
 checkCaseArms loc ((PBox x _, rhs) :: rest) =
   if null rest then pure $ CaseBox x rhs loc
   else fatalError "unexpected pattern after box"
+checkCaseArms loc ((PSup x y rh ih _, rhs) :: rest) =
+  if null rest then pure $ CaseW x y (rh, ih) rhs loc
+  else fatalError "unexpected pattern after sup"
 
 export
 caseBody : FileName -> Grammar True PCaseBody
@@ -557,8 +629,7 @@ caseTerm fname = withLoc fname $ do
 -- term : FileName -> Grammar True PTerm
 term fname = lamTerm fname
          <|> caseTerm fname
-         <|> piTerm fname
+         <|> bindTerm fname
-         <|> sigmaTerm fname
 
 
 export

lib/Quox/Parser/Syntax.idr

@@ -74,6 +74,9 @@ namespace PTerm
       | Pair PTerm PTerm Loc
       | Case PQty PTerm (PatVar, PTerm) PCaseBody Loc
 
+      | W PatVar PTerm PTerm Loc
+      | Sup PTerm PTerm Loc
+
       | Enum (List TagVal) Loc
       | Tag TagVal Loc
 
@@ -98,6 +101,7 @@ namespace PTerm
     public export
     data PCaseBody =
         CasePair (PatVar, PatVar) PTerm Loc
+      | CaseW PatVar PatVar (PQty, PatVar) PTerm Loc
       | CaseEnum (List (PTagVal, PTerm)) Loc
       | CaseNat PTerm (PatVar, PQty, PatVar, PTerm) Loc
       | CaseBox PatVar PTerm Loc
@@ -114,6 +118,8 @@ Located PTerm where
   (Sig  _ _ _         loc).loc = loc
   (Pair _ _           loc).loc = loc
   (Case _ _ _ _       loc).loc = loc
+  (W    _ _ _         loc).loc = loc
+  (Sup  _ _           loc).loc = loc
   (Enum _             loc).loc = loc
   (Tag  _             loc).loc = loc
   (Eq   _ _ _         loc).loc = loc
@@ -132,6 +138,7 @@ Located PTerm where
 export
 Located PCaseBody where
   (CasePair _ _     loc).loc = loc
+  (CaseW    _ _ _ _ loc).loc = loc
   (CaseEnum _       loc).loc = loc
   (CaseNat  _ _     loc).loc = loc
   (CaseBox  _ _     loc).loc = loc

lib/Quox/Pretty.idr

@@ -24,9 +24,13 @@ data PPrec
 = Outer
 | Times   -- "_ × _"
 | InTimes -- arguments of ×
+| W       -- "_ ⊲ _"
+| InW     -- arguments of ⊲
 | AnnL    -- left of "∷"
 | Eq      -- "_ ≡ _ : _"
 | InEq    -- arguments of ≡
+| Sup     -- "_ ⋄ _"
+| InSup   -- arguments of ⋄
   -- ...
 | App  -- term/dimension application
 | Arg  -- argument to nonfix function
@@ -229,10 +233,10 @@ prettyDBind = hl DVar . prettyBind'
 
 
 export %inline
-typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD,
+typeD, arrowD, darrowD, timesD, lamD, eqndD, dlamD, annD, natD, triD, diamondD,
-eqD, colonD, commaD, semiD, caseD, typecaseD, returnD,
+eqD, colonD, commaD, semiD, caseD, typecaseD, returnD, ofD, dotD, zeroD, succD,
-ofD, dotD, zeroD, succD, coeD, compD, undD, cstD, pipeD :
+coeD, compD, undD, cstD, pipeD :
-  {opts : _} -> Eff Pretty (Doc opts)
+  {opts : LayoutOpts} -> Eff Pretty (Doc opts)
 typeD     = hl Syntax . text =<< ifUnicode "★" "Type"
 arrowD    = hl Delim  . text =<< ifUnicode "→" "->"
 darrowD   = hl Delim  . text =<< ifUnicode "⇒" "=>"
@@ -242,6 +246,8 @@ eqndD     = hl Delim  . text =<< ifUnicode "≡" "=="
 dlamD     = hl Syntax . text =<< ifUnicode "δ" "dfun"
 annD      = hl Delim  . text =<< ifUnicode "∷" "::"
 natD      = hl Syntax . text =<< ifUnicode "ℕ" "Nat"
+triD      = hl Syntax . text =<< ifUnicode "⊲" "<|"
+diamondD  = hl Syntax . text =<< ifUnicode "⋄" "<>"
 eqD       = hl Syntax $ text "Eq"
 colonD    = hl Delim  $ text ":"
 commaD    = hl Delim  $ text ","

lib/Quox/Reduce.idr

@@ -78,6 +78,12 @@ isPairHead (Ann (Pair {}) (Sig {}) _) = True
 isPairHead (Coe {})                   = True
 isPairHead _                          = False
 
+public export %inline
+isWHead : Elim {} -> Bool
+isWHead (Ann (Sup {}) (W {}) _) = True
+isWHead (Coe {})                = True
+isWHead _                       = False
+
 public export %inline
 isTagHead : Elim {} -> Bool
 isTagHead (Ann (Tag {}) (Enum {}) _) = True
@@ -115,6 +121,8 @@ isTyCon (Pi    {}) = True
 isTyCon (Lam   {}) = False
 isTyCon (Sig   {}) = True
 isTyCon (Pair  {}) = False
+isTyCon (W     {}) = True
+isTyCon (Sup   {}) = False
 isTyCon (Enum  {}) = True
 isTyCon (Tag   {}) = False
 isTyCon (Eq    {}) = True
@@ -128,6 +136,37 @@ isTyCon (E     {}) = False
 isTyCon (CloT  {}) = False
 isTyCon (DCloT {}) = False
 
+||| canPushCoe A s is true if a coercion along (𝑖 ⇒ A) on s can be pushed.
+||| for a type with η like functions, or a ground type like ℕ,
+||| this is true for any s.
+||| otherwise, like for pairs, it is only true if s is a constructor form.
+||| if A isn't a type, or isn't in whnf, then the question is meaningless. but
+||| it returns False anyway.
+public export %inline
+canPushCoe : Term (S d) n -> Term d n -> Bool
+canPushCoe (TYPE  {}) _         = True
+canPushCoe (Pi    {}) _         = True
+canPushCoe (Lam   {}) _         = False
+canPushCoe (Sig   {}) (Pair {}) = True
+canPushCoe (Sig   {}) _         = False
+canPushCoe (Pair  {}) _         = False
+canPushCoe (W     {}) (Sup {})  = True
+canPushCoe (W     {}) _         = False
+canPushCoe (Sup   {}) _         = False
+canPushCoe (Enum  {}) _         = True
+canPushCoe (Tag   {}) _         = False
+canPushCoe (Eq    {}) _         = True
+canPushCoe (DLam  {}) _         = False
+canPushCoe (Nat   {}) _         = True
+canPushCoe (Zero  {}) _         = False
+canPushCoe (Succ  {}) _         = False
+canPushCoe (BOX   {}) _         = True
+canPushCoe (Box   {}) _         = False
+canPushCoe (E     {}) _         = False
+canPushCoe (CloT  {}) _         = False
+canPushCoe (DCloT {}) _         = False
+
+
 ||| true if a term is syntactically a type, or a neutral.
 public export %inline
 isTyConE : Term {} -> Bool
@@ -155,6 +194,8 @@ mutual
     isRedexE defs fun || isLamHead fun
   isRedexE defs (CasePair {pair, _}) =
     isRedexE defs pair || isPairHead pair
+  isRedexE defs (CaseW {tree, _}) =
+    isRedexE defs tree || isWHead tree
   isRedexE defs (CaseEnum {tag, _}) =
     isRedexE defs tag || isTagHead tag
   isRedexE defs (CaseNat {nat, _}) =
@@ -165,8 +206,9 @@ mutual
     isRedexE defs fun || isDLamHead fun || isK arg
   isRedexE defs (Ann {tm, ty, _}) =
     isE tm || isRedexT defs tm || isRedexT defs ty
-  isRedexE defs (Coe {val, _}) =
+  isRedexE defs (Coe {ty, val, _}) =
-    isRedexT defs val || not (isE val)
+    let ty = assert_smaller ty ty.term in
+    isRedexT defs ty || canPushCoe ty val
   isRedexE defs (Comp {ty, r, _}) =
     isRedexT defs ty || isK r
   isRedexE defs (TypeCase {ty, ret, _}) =
@@ -204,17 +246,37 @@ tycaseRhsDef0 : Term d n -> (k : TyConKind) -> TypeCaseArms d n ->
 tycaseRhsDef0 def k arms = fromMaybe def $ tycaseRhs0 k arms
 
 
+export
+weakAtT : (CanTSubst f, Located2 f) => (by, at : Nat) ->
+          f d (at + n) -> f d (at + (by + n))
+weakAtT by at t = t `CanTSubst.(//)` pushN at (shift by) t.loc
 
-private
+export
-weakDS : (by : Nat) -> DScopeTerm d n -> DScopeTerm d (by + n)
+weakAtD : (CanDSubst f, Located2 f) => (by, at : Nat) ->
+          f (at + d) n -> f (at + (by + d)) n
+weakAtD by at t = t `CanDSubst.(//)` pushN at (shift by) t.loc
+
+parameters {s : Nat}
+  export
+  weakS : (by : Nat) -> ScopeTermN s d n -> ScopeTermN s d (by + n)
+  weakS by (S names (Y body)) = S names $ Y $ weakAtT by s body
+  weakS by (S names (N body)) = S names $ N $ weakT by body
+
+  export
+  weakDS : (by : Nat) -> DScopeTermN s d n -> DScopeTermN s d (by + n)
   weakDS by (S names (Y body)) = S names $ Y $ weakT by body
   weakDS by (S names (N body)) = S names $ N $ weakT by body
 
-private
+  export
-dweakS : (by : Nat) -> ScopeTerm d n -> ScopeTerm (by + d) n
+  dweakS : (by : Nat) -> ScopeTermN s d n -> ScopeTermN s (by + d) n
   dweakS by (S names (Y body)) = S names $ Y $ dweakT by body
   dweakS by (S names (N body)) = S names $ N $ dweakT by body
 
+  export
+  dweakDS : (by : Nat) -> DScopeTermN s d n -> DScopeTermN s (by + d) n
+  dweakDS by (S names (Y body)) = S names $ Y $ weakAtD by s body
+  dweakDS by (S names (N body)) = S names $ N $ dweakT by body
+
 private
 coeScoped : {s : Nat} -> DScopeTerm d n -> Dim d -> Dim d -> Loc ->
             ScopeTermN s d n -> ScopeTermN s d n
@@ -246,6 +308,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
       | t => throw $ ExpectedPi loc ctx.names t
     pure $ sub1 res $ Ann s arg loc
   computeElimType (CasePair {pair, ret, _}) = pure $ sub1 ret pair
+  computeElimType (CaseW {tree, ret, _}) = pure $ sub1 ret tree
   computeElimType (CaseEnum {tag, ret, _}) = pure $ sub1 ret tag
   computeElimType (CaseNat {nat, ret, _}) = pure $ sub1 ret nat
   computeElimType (CaseBox {box, ret, _}) = pure $ sub1 ret box
@@ -269,7 +332,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   tycasePi (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
     let loc  = e.loc
-        narg = mnb "Arg"; nret = mnb "Ret"
+        narg = mnb "Arg" loc; nret = mnb "Ret" loc
         arg  = E $ typeCase1Y e ty KPi [< !narg, !nret] (BVT 1 loc) loc
         res' = typeCase1Y e (Arr Zero arg ty loc) KPi [< !narg, !nret]
                  (BVT 0 loc) loc
@@ -287,7 +350,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   tycaseSig (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
     let loc  = e.loc
-        nfst = mnb "Fst"; nsnd = mnb "Snd"
+        nfst = mnb "Fst" loc; nsnd = mnb "Snd" loc
         fst  = E $ typeCase1Y e ty KSig [< !nfst, !nsnd] (BVT 1 loc) loc
         snd' = typeCase1Y e (Arr Zero fst ty loc) KSig [< !nfst, !nsnd]
                  (BVT 0 loc) loc
@@ -295,6 +358,24 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
     pure (fst, snd)
   tycaseSig t = throw $ ExpectedSig t.loc ctx.names t
 
+  ||| for (x : A) ⊲ B, returns (A, B);
+  ||| for an elim returns a pair of type-cases that will reduce to that;
+  ||| for other intro forms error
+  private covering
+  tycaseW : (t : Term (S d) n) -> (0 tnf : No (isRedexT defs t)) =>
+            Eff Whnf (Term (S d) n, ScopeTerm (S d) n)
+  tycaseW (W {shape, body, _}) = pure (shape, body)
+  tycaseW (E e) {tnf} = do
+    ty <- computeElimType defs ctx e @{noOr2 tnf}
+    let loc    = e.loc
+        nshape = mnb "Shape" loc; nbody = mnb "Body" loc
+        shape  = E $ typeCase1Y e ty KW [< !nshape, !nbody] (BVT 1 loc) loc
+        body'  = typeCase1Y e (Arr Zero shape ty loc) KW [< !nshape, !nbody]
+                   (BVT 0 loc) loc
+        body   = ST [< !nshape] $ E $ App (weakE 1 body') (BVT 0 loc) loc
+    pure (shape, body)
+  tycaseW t = throw $ ExpectedW t.loc ctx.names t
+
   ||| for [π. A], returns A;
   ||| for an elim returns a type-case that will reduce to that;
   ||| for other intro forms error
@@ -303,8 +384,9 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
               Eff Whnf (Term (S d) n)
   tycaseBOX (BOX {ty, _}) = pure ty
   tycaseBOX (E e) {tnf} = do
+    let loc = e.loc
     ty <- computeElimType defs ctx e @{noOr2 tnf}
-    pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty")] (BVT 0 e.loc) e.loc
+    pure $ E $ typeCase1Y e ty KBOX [< !(mnb "Ty" loc)] (BVT 0 loc) loc
   tycaseBOX t = throw $ ExpectedBOX t.loc ctx.names t
 
   ||| for Eq [i ⇒ A] l r, returns (A‹0/i›, A‹1/i›, A, l, r);
@@ -318,11 +400,11 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext (S d) n)
   tycaseEq (E e) {tnf} = do
     ty <- computeElimType defs ctx e @{noOr2 tnf}
     let loc   = e.loc
-        names = traverse' (\x => mnb x) [< "A0", "A1", "A", "L", "R"]
+        names = traverse' (\x => mnb x loc) [< "A0", "A1", "A", "l", "r"]
         a0    = E $ typeCase1Y e ty KEq !names (BVT 4 loc) loc
         a1    = E $ typeCase1Y e ty KEq !names (BVT 3 loc) loc
         a'    = typeCase1Y e (Eq0 ty a0 a1 loc) KEq !names (BVT 2 loc) loc
-        a     = DST [< !(mnb "i")] $ E $ DApp (dweakE 1 a') (B VZ loc) loc
+        a     = DST [< !(mnb "i" loc)] $ E $ DApp (dweakE 1 a') (B VZ loc) loc
         l     = E $ typeCase1Y e a0 KEq !names (BVT 1 loc) loc
         r     = E $ typeCase1Y e a1 KEq !names (BVT 0 loc) loc
     pure (a0, a1, a, l, r)
@@ -337,9 +419,12 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
           (val, s : Term d n) -> Loc ->
           Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
   piCoe sty@(S [< i] ty) p q val s loc = do
-    -- (coe [i ⇒ π.(x : A) → B] @p @q t) s ⇝
+    --  𝒮‹𝑘› ≔ π.(x : A‹𝑘/𝑖›) → B‹𝑘/𝑖›
-    -- coe [i ⇒ B[𝒔‹i›/x] @p @q ((t ∷ (π.(x : A) → B)‹p/i›) 𝒔‹p›)
+    --  𝓈‹𝑘› ≔ coe [𝑖 ⇒ A] @q @𝑘 s
-    --   where 𝒔‹j› ≔ coe [i ⇒ A] @q @j s
+    -- -------------------------------------------------------
+    --  (coe [𝑖 ⇒ 𝒮‹𝑖›] @p @q t) s
+    --    ⇝
+    --  coe [i ⇒ B[𝓈‹i›/x] @p @q ((t ∷ 𝒮‹p›) 𝓈‹p›)
     --
     -- type-case is used to expose A,B if the type is neutral
     let ctx1 = extendDim i ctx
@@ -358,11 +443,11 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
            (ret : ScopeTerm d n) -> (body : ScopeTermN 2 d n) -> Loc ->
            Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
   sigCoe qty sty@(S [< i] ty) p q val ret body loc = do
-    -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ e }
+    -- caseπ (coe [i ⇒ (x : A) × B] @p @q s) return z ⇒ C of { (a, b) ⇒ u }
     -- ⇝
     -- caseπ s ∷ ((x : A) × B)‹p/i› return z ⇒ C
     -- of { (a, b) ⇒
-    --   e[(coe [i ⇒ A] @p @q a)/a,
+    --   u[(coe [i ⇒ A] @p @q a)/a,
     --     (coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i a)/x]] @p @q b)/b] }
     --
     -- type-case is used to expose A,B if the type is neutral
@@ -370,14 +455,58 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
     Element ty tynf <- whnf defs ctx1 ty.term
     (tfst, tsnd) <- tycaseSig defs ctx1 ty
     let [< x, y] = body.names
-        a' = CoeT i (weakT 2 tfst) p q (BVT 1 noLoc) x.loc
+        a' = CoeT i (weakT 2 tfst) p q (BVT 1 x.loc) x.loc
         tsnd' = tsnd.term //
-          (CoeT i (weakT 2 $ tfst // (B VZ noLoc ::: shift 2))
+          (CoeT !(fresh i) (weakT 2 $ tfst // (B VZ i.loc ::: shift 2))
-            (weakD 1 p) (B VZ noLoc) (BVT 1 noLoc) y.loc ::: shift 2)
+            (weakD 1 p) (B VZ i.loc) (BVT 1 x.loc) y.loc ::: shift 2)
-        b' = CoeT i tsnd' p q (BVT 0 noLoc) y.loc
+        b' = CoeT i tsnd' p q (BVT 0 y.loc) y.loc
-    whnf defs ctx $ CasePair qty (Ann val (ty // one p) val.loc) ret
+    whnf defs ctx $ CasePair qty (Ann val (dsub1 sty p) val.loc) ret
       (ST body.names $ body.term // (a' ::: b' ::: shift 2)) loc
 
+  ||| reduce a w elimination `CaseW pi piIH (Coe ty p q val) ret body loc`
+  private covering
+  wCoe : (qty, qtyIH : Qty) ->
+         (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
+         (ret : ScopeTerm d n) -> (body : ScopeTermN 3 d n) -> Loc ->
+         Eff Whnf (Subset (Elim d n) (No . isRedexE defs))
+  wCoe qty qtyIH sty@(S [< i] ty) p q val ret body loc = do
+    --  𝒮‹𝑘› ≔ ((x : A) ⊲ B)‹𝑘/𝑖›
+    --  𝒶‹𝑘› ≔ coe [𝑖 ⇒ A] @p @𝑘 a
+    --       : A‹𝑘/𝑖›
+    --  𝒷‹𝑘› ≔ coe [𝑖 ⇒ ω.B[𝒶‹𝑖›/x] → 𝒮‹𝑖›] @p @𝑘 b
+    --       : ω.B‹𝑘/𝑖›[𝒶‹𝑘›/x] → 𝒮‹𝑘›
+    --  𝒾𝒽   ≔ coe [𝑖 ⇒ π.(z : B[𝒶‹𝑖›/x]) → C[𝒷‹𝑖› z/p]] @p @q ih
+    --       : π.(z : B‹q/𝑖›[𝒶‹q›/x]) → C[𝒷‹q› z/p]
+    -- --------------------------------------------------------------------
+    --  caseπ (coe [𝑖 ⇒ 𝒮‹𝑖›] @p @q s) return z ⇒ C of { a ⋄ b, ς.ih ⇒ u }
+    --    ⇝
+    --  caseπ s ∷ 𝒮‹p› return z ⇒ C
+    --  of { a ⋄ b, ς.ih ⇒ u[𝒶‹q›/a, 𝒷‹q›/b, 𝒾𝒽/ih] }
+    let ctx1 = extendDim i ctx
+    Element ty tynf <- whnf defs ctx1 ty.term
+    (shape, tbody) <- tycaseW defs ctx1 ty
+    let [< a, b, ih] = body.names
+    ai <- fresh i; bi <- fresh i; ihi <- fresh i; z <- mnb "z" ih.loc
+    let a', b' : forall d'. (by : Shift d d') => Dim d' -> Elim d' (3 + n)
+        a' k =
+          let shape' = shape // Shift (weak 1 by) // shift 3 in
+          CoeT ai shape' (p // by) k (BVT 2 a.loc) a.loc
+        b' k =
+          let tbody' = tbody.term // Shift (weak 1 by)
+                                  // (a' (BV 0 bi.loc) ::: shift 3)
+              ty' = ty // Shift (weak 1 by) // shift 3
+          in
+          CoeT bi (Arr Any tbody' ty' b.loc) (p // by) k (BVT 1 b.loc) b.loc
+        ih' : Elim d (3 + n) :=
+          let tbody' = tbody.term // (a' (BV 0 ihi.loc) ::: shift 3)
+              ret' = sub1 (weakS 4 $ dweakS 1 ret) $
+                     App (weakE 1 $ b' (BV 0 ihi.loc)) (BVT 0 z.loc) ih.loc
+              ty = PiY qty z tbody' ret' ih.loc
+          in
+          CoeT ihi ty p q (BVT 0 ih.loc) ih.loc
+    whnf defs ctx $ CaseW qty qtyIH (Ann val (dsub1 sty p) val.loc) ret
+      (ST body.names $ body.term // (a' q ::: b' q ::: ih' ::: shift 3)) loc
+
   ||| reduce a dimension application `DApp (Coe ty p q val) r loc`
   private covering
   eqCoe : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
@@ -392,7 +521,7 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
     Element ty tynf <- whnf defs ctx1 ty.term
     (a0, a1, a, s, t) <- tycaseEq defs ctx1 ty
     let a'   = dsub1 a (weakD 1 r)
-        val' = E $ DApp (Ann val (ty // one p) val.loc) r loc
+        val' = E $ DApp (Ann val (dsub1 sty p) val.loc) r loc
     whnf defs ctx $ CompH j a' p q val' r j s j t loc
 
   ||| reduce a pair elimination `CaseBox pi (Coe ty p q val) ret body`
@@ -409,8 +538,8 @@ parameters {d, n : Nat} (defs : Definitions) (ctx : WhnfContext d n)
     let ctx1 = extendDim i ctx
     Element ty tynf <- whnf defs ctx1 ty.term
     ta <- tycaseBOX defs ctx1 ty
-    let a' = CoeT i (weakT 1 ta) p q (BVT 0 noLoc) body.name.loc
+    let a' = CoeT i (weakT 1 ta) p q (BVT 0 body.name.loc) body.name.loc
-    whnf defs ctx $ CaseBox qty (Ann val (ty // one p) val.loc) ret
+    whnf defs ctx $ CaseBox qty (Ann val (dsub1 sty p) val.loc) ret
       (ST body.names $ body.term // (a' ::: shift 1)) loc
 
 
@@ -429,19 +558,29 @@ reduceTypeCase defs ctx ty u ret arms def loc = case ty of
   -- (type-case π.(x : A) → B ∷ ★ᵢ return Q of { (a → b) ⇒ s; ⋯ }) ⇝
   -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
   Pi {arg, res, loc = piLoc, _} =>
-    let arg' = Ann arg (TYPE u noLoc) arg.loc
+    let arg' = Ann arg (TYPE u arg.loc) arg.loc
         res' = Ann (Lam res res.loc)
-                   (Arr Zero arg (TYPE u noLoc) arg.loc) res.loc
+                   (Arr Zero arg (TYPE u arg.loc) arg.loc) res.loc
     in
     whnf defs ctx $
       Ann (subN (tycaseRhsDef def KPi arms) [< arg', res']) ret loc
 
+  -- (type-case (x : A) ⊲ π.B ∷ ★ᵢ return Q of { (a ⊲ b) ⇒ s; ⋯ }) ⇝
+  -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
+  W {shape, body, loc = wLoc, _} =>
+    let shape' = Ann shape (TYPE u shape.loc) shape.loc
+        body'  = Ann (Lam body body.loc)
+                     (Arr Zero shape (TYPE u shape.loc) shape.loc) body.loc
+    in
+    whnf defs ctx $
+      Ann (subN (tycaseRhsDef def KW arms) [< shape', body']) ret loc
+
   -- (type-case (x : A) × B ∷ ★ᵢ return Q of { (a × b) ⇒ s; ⋯ }) ⇝
   -- s[(A ∷ ★ᵢ)/a, ((λ x ⇒ B) ∷ 0.A → ★ᵢ)/b] ∷ Q
   Sig {fst, snd, loc = sigLoc, _} =>
-    let fst' = Ann fst (TYPE u noLoc) fst.loc
+    let fst' = Ann fst (TYPE u fst.loc) fst.loc
         snd' = Ann (Lam snd snd.loc)
-                   (Arr Zero fst (TYPE u noLoc) fst.loc) snd.loc
+                   (Arr Zero fst (TYPE u fst.loc) fst.loc) snd.loc
     in
     whnf defs ctx $
       Ann (subN (tycaseRhsDef def KSig arms) [< fst', snd']) ret loc
@@ -459,8 +598,8 @@ reduceTypeCase defs ctx ty u ret arms def loc = case ty of
     let a0 = a.zero; a1 = a.one in
     whnf defs ctx $ Ann
       (subN (tycaseRhsDef def KEq arms)
-         [< Ann a0 (TYPE u noLoc) a.loc, Ann a1 (TYPE u noLoc) a.loc,
+         [< Ann a0 (TYPE u a.loc) a.loc, Ann a1 (TYPE u a.loc) a.loc,
-            Ann (DLam a a.loc) (Eq0 (TYPE u noLoc) a0 a1 a.loc) a.loc,
+            Ann (DLam a a.loc) (Eq0 (TYPE u a.loc) a0 a1 a.loc) a.loc,
             Ann l a0 l.loc, Ann r a1 r.loc])
       ret loc
 
@@ -471,99 +610,113 @@ reduceTypeCase defs ctx ty u ret arms def loc = case ty of
   -- (type-case [π.A] ∷ ★ᵢ return Q of { [a] ⇒ s; ⋯ }) ⇝ s[(A ∷ ★ᵢ)/a] ∷ Q
   BOX {ty = a, loc = boxLoc, _} =>
     whnf defs ctx $ Ann
-      (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u noLoc) a.loc))
+      (sub1 (tycaseRhsDef def KBOX arms) (Ann a (TYPE u a.loc) a.loc))
       ret loc
 
 
 ||| pushes a coercion inside a whnf-ed term
 private covering
 pushCoe : {d, n : Nat} -> (defs : Definitions) -> WhnfContext d n ->
-          BindName ->
+          BindName -> (ty : Term (S d) n) ->
-          (ty : Term (S d) n) -> (0 tynf : No (isRedexT defs ty)) =>
           Dim d -> Dim d ->
-          (s : Term d n) -> (0 snf : No (isRedexT defs s)) => Loc ->
+          (s : Term d n) -> (0 snf : No (isRedexT defs s)) =>
+          (0 pc : So (canPushCoe ty s)) => Loc ->
           Eff Whnf (NonRedex Elim d n defs)
 pushCoe defs ctx i ty p q s loc =
   if p == q then whnf defs ctx $ Ann s (ty // one q) loc else
-  case s of
+  case ty of
-    -- (coe [_ ⇒ ★ᵢ] @_ @_ ty) ⇝ (ty ∷ ★ᵢ)
+    -- (coe ★ᵢ @p @q s) ⇝ (s ∷ ★ᵢ)
-    TYPE {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
+    --
-    Pi   {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
+    -- no η (what would that even mean), but ground type
-    Sig  {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
+    TYPE {l, loc = tyLoc} =>
-    Enum {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
+      whnf defs ctx $ Ann s (TYPE l tyLoc) loc
-    Eq   {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
-    Nat  {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
-    BOX  {} => pure $ nred $ Ann s (TYPE !(unwrapTYPE ty) ty.loc) loc
 
     -- just η expand it. then whnf for App will handle it later
     -- this is how @xtt does it
     --
-    -- (coe [i ⇒ A] @p @q (λ x ⇒ s)) ⇝
+    -- (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) ⇝
-    -- (λ y ⇒ (coe [i ⇒ A] @p @q (λ x ⇒ s)) y) ∷ A‹q/i› ⇝ ⋯
+    -- (λ y ⇒ (coe (𝑖 ⇒ π.(x : A) → B) @p @q s) y)
-    lam@(Lam {body, _}) => do
+    --   ∷ (π.(x : A) → B)‹q/𝑖›
-      let lam'  = CoeT i ty p q lam loc
+    Pi {} => do
-          term' = LamY !(fresh body.name)
+      y <- mnb "y" loc
-                    (E $ App (weakE 1 lam') (BVT 0 noLoc) loc) loc
+      let s'   = Coe (SY [< i] ty) p q s loc
-          type' = ty // one q
+          body = SY [< y] $ E $ App (weakE 1 s') (BVT 0 y.loc) s.loc
-      whnf defs ctx $ Ann term' type' loc
+          ret  = ty // one q
+      whnf defs ctx $ Ann (Lam body loc) ret loc
 
     -- (coe [i ⇒ (x : A) × B] @p @q (s, t)) ⇝
     -- (coe [i ⇒ A] @p @q s,
     --  coe [i ⇒ B[(coe [j ⇒ A‹j/i›] @p @i s)/x]] @p @q t)
     --   ∷ (x : A‹q/i›) × B‹q/i›
     --
-    -- can't use η here because... it doesn't exist
+    -- no η so only reduce on an actual pair 🍐
-    Pair {fst, snd, loc = pairLoc} => do
+    Sig {fst = tfst, snd = tsnd, loc = tyLoc} => do
-      let Sig {fst = tfst, snd = tsnd, loc = sigLoc} = ty
+      let Pair fst snd sLoc = s
-        | _ => throw $ ExpectedSig ty.loc (extendDim i ctx.names) ty
+          fst'  = E $ CoeT i tfst p q fst fst.loc
-      let fst'  = E $ CoeT i tfst p q fst fst.loc
+          tfst' = tfst // (B VZ i.loc ::: shift 2)
-          tfst' = tfst // (B VZ noLoc ::: shift 2)
           tsnd' = sub1 tsnd $
-                  CoeT !(fresh i) tfst' (weakD 1 p) (B VZ noLoc)
+                  CoeT !(fresh i) tfst' (weakD 1 p) (B VZ snd.loc)
-                    (dweakT 1 fst) fst.loc
+                    (dweakT 1 fst) snd.loc
           snd'  = E $ CoeT i tsnd' p q snd snd.loc
-      pure $
+      pure $ nred $
-        Element (Ann (Pair fst' snd' pairLoc)
+        Ann (Pair fst' snd' sLoc)
-                     (Sig (tfst // one q) (tsnd // one q) sigLoc) loc) Ah
+            (Sig (tfst // one q) (tsnd // one q) tyLoc) loc
+
+    -- (coe [i ⇒ (x : A) ⊲ π.B] @p @q (s ⋄ t) ⇝
+    -- (coe [i ⇒ A] @p @q s ⋄
+    --  coe [i ⇒ ω.B[coe [j ⇒ A‹j/i›] @p @i s/x] → (x : A) ⊲ B] t)
+    --   ∷ ((x : A) ⊲ B)‹q/i›
+    --
+    -- again, no η
+    W {shape, body, loc = tyLoc} => do
+      let Sup root sub sLoc = s
+          root' = E $ CoeT i shape p q root root.loc
+          shape' = shape // (B VZ i.loc ::: shift 2)
+          coeRoot =
+            CoeT (setLoc shape.loc !(fresh i)) shape'
+                 (weakD 1 p) (B VZ i.loc) (dweakT 1 root) root.loc
+          tsub' = Arr Any (sub1 body coeRoot) ty sub.loc
+          sub' = E $ CoeT i tsub' p q sub sub.loc
+      pure $ nred $
+        Ann (Sup root' sub' sLoc)
+            (W (shape // one q) (body // one q) tyLoc) loc
+
+    -- (coe {𝗮, …} @p @q s) ⇝ (s ∷ {𝗮, …})
+    --
+    -- no η, but ground type
+    Enum {cases, loc = tyLoc} =>
+      whnf defs ctx $ Ann s (Enum cases tyLoc) loc
 
     -- η expand, like for Lam
     --
-    -- (coe [i ⇒ A] @p @q (δ j ⇒ s)) ⇝
+    -- (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) ⇝
-    -- (δ k ⇒ (coe [i ⇒ A] @p @q (δ j ⇒ s)) @k) ∷ A‹q/i› ⇝ ⋯
+    -- (δ k ⇒ (coe (𝑖 ⇒ Eq (𝑗 ⇒ A) l r) @p @q s) @k)
-    dlam@(DLam {body, _}) => do
+    --   ∷ (Eq (𝑗 ⇒ A) l r)‹q/𝑖›
-      let dlam' = CoeT i ty p q dlam loc
+    Eq {} => do
-          term' = DLamY !(mnb "j")
+      k <- mnb "k" loc
-                    (E $ DApp (dweakE 1 dlam') (B VZ noLoc) loc) loc
+      let s'   = Coe (SY [< i] ty) p q s loc
-          type' = ty // one q
+          term = DLam (SY [< k] $ E $ DApp (dweakE 1 s') (BV 0 k.loc) loc) loc
-      whnf defs ctx $ Ann term' type' loc
+          ret  = ty // one q
+      whnf defs ctx $ Ann term ret loc
 
-    -- (coe [_ ⇒ {⋯}] @_ @_ t) ⇝ (t ∷ {⋯})
+    -- (coe ℕ @p @q s) ⇝ (s ∷ ℕ)
-    Tag {tag, loc = tagLoc} => do
+    --
-      let Enum {cases, loc = enumLoc} = ty
+    -- no η, but ground type
-        | _ => throw $ ExpectedEnum ty.loc (extendDim i ctx.names) ty
+    Nat {loc = tyLoc} =>
-      pure $ Element (Ann (Tag tag tagLoc) (Enum cases enumLoc) loc) Ah
+      whnf defs ctx $ Ann s (Nat tyLoc) loc
 
-    -- (coe [_ ⇒ ℕ] @_ @_ n) ⇝ (n ∷ ℕ)
+    -- (coe (𝑖 ⇒ [π. A]) @p @q s) ⇝
-    Zero {loc = zeroLoc} => do
+    -- [coe (𝑖 ⇒ A) @p @q (case1 s ∷ [π. A‹p/𝑖›] return A‹p/𝑖› of {[x] ⇒ x})]
-      pure $ Element (Ann (Zero zeroLoc) (Nat ty.loc) loc) Ah
+    --   ∷ [π. A‹q/𝑖›]
-    Succ {p = pred, loc = succLoc} => do
+    --
-      pure $ Element (Ann (Succ pred succLoc) (Nat ty.loc) loc) Ah
+    -- [todo] box should probably have an η rule
-
+    BOX {qty, ty = innerTy, loc = tyLoc} => do
-    -- (coe [i ⇒ [π.A]] @p @q [s]) ⇝
+      let s'     = Ann s (BOX qty (innerTy // one p) tyLoc) s.loc
-    -- [coe [i ⇒ A] @p @q s] ∷ [π. A‹q/i›]
+          inner' = CaseBox One s' (SN $ innerTy // one p)
-    Box {val, loc = boxLoc} => do
+                     (SY [< !(mnb "x" s.loc)] $ BVT 0 s.loc) s.loc
-      let BOX {qty, ty = a, loc = tyLoc} = ty
+          inner  = Box (E $ CoeT i innerTy p q (E inner') loc) loc
-        | _ => throw $ ExpectedBOX ty.loc (extendDim i ctx.names) ty
+          ret    = BOX qty (innerTy // one q) tyLoc
-      pure $ Element
+      whnf defs ctx $ Ann inner ret loc
-        (Ann (Box (E $ CoeT i a p q val val.loc) boxLoc)
-             (BOX qty (a // one q) tyLoc) loc)
-        Ah
-
-    E e => pure $ Element (CoeT i ty p q (E e) e.loc) (snf `orNo` Ah)
-where
-  unwrapTYPE : Term (S d) n -> Eff Whnf Universe
-  unwrapTYPE (TYPE {l, _}) = pure l
-  unwrapTYPE ty = throw $ ExpectedTYPE ty.loc (extendDim i ctx.names) ty
 
 
 export covering
@@ -585,8 +738,12 @@ CanWhnf Elim Reduce.isRedexE where
         Coe ty p q val _ => piCoe defs ctx ty p q val s appLoc
       Right nlh => pure $ Element (App f s appLoc) $ fnf `orNo` nlh
 
-  -- case (s, t) ∷ (x : A) × B return p ⇒ C of { (a, b) ⇒ u } ⇝
+  --  s'  ≔ s ∷ A
-  -- u[s∷A/a, t∷B[s∷A/x]] ∷ C[(s, t)∷((x : A) × B)/p]
+  --  t'  ≔ t ∷ B[s'/x]
+  --  st' ≔ (s, t) ∷ (x : A) × B
+  --  C'  ≔ C[st'/p]
+  -- ---------------------------------------------------------------
+  --  case st' return p ⇒ C of { (a, b) ⇒ u } ⇝ u[s'/a, t'/x]] ∷ C'
   whnf defs ctx (CasePair pi pair ret body caseLoc) = do
     Element pair pairnf <- whnf defs ctx pair
     case nchoose $ isPairHead pair of
@@ -601,6 +758,43 @@ CanWhnf Elim Reduce.isRedexE where
       Right np =>
         pure $ Element (CasePair pi pair ret body caseLoc) $ pairnf `orNo` np
 
+  --  s'  ≔ s ∷ A
+  --  t'  ≔ t ∷ ω.B[s'/x] → (x : A) ⊲ B
+  --  ih' ≔ (λ x ⇒ caseπ t x return p ⇒ C of { (a ⋄ b), ς.ih ⇒ u }) ∷
+  --          π.(y : B[s'/x]) → C[t' y/p]
+  --  st' ≔ s ⋄ t ∷ (x : A) ⊲ B
+  --  C'  ≔ C[st'/p]
+  -- --------------------------------------------------------------------
+  --  caseπ st' return p ⇒ C of { a ⋄ b, ς.ih ⇒ u }
+  --   ⇝
+  --  u[s'/a, t'/b, ih'/ih] ∷ C'
+  whnf defs ctx (CaseW qty qtyIH tree ret body caseLoc) = do
+    Element tree treenf <- whnf defs ctx tree
+    case nchoose $ isWHead tree of
+      Left _ => case tree of
+        Ann (Sup {root, sub, _})
+            w@(W {shape, body = wbody, _}) treeLoc =>
+          let root = Ann root shape root.loc
+              wbody' = sub1 wbody root
+              tsub = Arr Any wbody' w sub.loc
+              sub = Ann sub tsub sub.loc
+              ih' = LamY !(mnb "y" caseLoc) -- [todo] better name
+                    (E $ CaseW qty qtyIH
+                           (App (weakE 1 sub) (BVT 0 sub.loc) sub.loc)
+                           (weakS 1 ret) (weakS 1 body) caseLoc) sub.loc
+              ihret = sub1 (weakS 1 ret)
+                           (App (weakE 1 sub) (BVT 0 sub.loc) caseLoc)
+              tih = PiY qty !(mnb "y" caseLoc)
+                      wbody' ihret caseLoc
+              ih = Ann ih' tih caseLoc
+          in
+          whnf defs ctx $
+          Ann (subN body [< root, sub, ih]) (sub1 ret tree) tree.loc
+        Coe ty p q val _ => do
+          wCoe defs ctx qty qtyIH ty p q val ret body caseLoc
+      Right nw => pure $
+        Element (CaseW qty qtyIH tree ret body caseLoc) $ treenf `orNo` nw
+
   -- case 'a ∷ {a,…} return p ⇒ C of { 'a ⇒ u } ⇝
   -- u ∷ C['a∷{a,…}/p]
   whnf defs ctx (CaseEnum pi tag ret arms caseLoc) = do
@@ -695,7 +889,10 @@ CanWhnf Elim Reduce.isRedexE where
   whnf defs ctx (Coe (S [< i] (Y ty)) p q val coeLoc) = do
     Element ty  tynf  <- whnf defs (extendDim i ctx) ty
     Element val valnf <- whnf defs ctx val
-    pushCoe defs ctx i ty p q val coeLoc
+    case nchoose $ canPushCoe ty val of
+      Right n => pure $ Element (Coe (SY [< i] ty) p q val coeLoc) $
+                        tynf `orNo` n
+      Left  y => pushCoe defs ctx i ty p q val coeLoc
 
   whnf defs ctx (Comp ty p q val r zero one compLoc) =
     -- comp [A] @p @p s { ⋯ } ⇝ s ∷ A
@@ -730,6 +927,8 @@ CanWhnf Term Reduce.isRedexT where
   whnf _ _ t@(Lam  {}) = pure $ nred t
   whnf _ _ t@(Sig  {}) = pure $ nred t
   whnf _ _ t@(Pair {}) = pure $ nred t
+  whnf _ _ t@(W    {}) = pure $ nred t
+  whnf _ _ t@(Sup  {}) = pure $ nred t
   whnf _ _ t@(Enum {}) = pure $ nred t
   whnf _ _ t@(Tag  {}) = pure $ nred t
   whnf _ _ t@(Eq   {}) = pure $ nred t

lib/Quox/Syntax/Dim.idr

@@ -83,7 +83,7 @@ DSubst : Nat -> Nat -> Type
 DSubst = Subst Dim
 
 
-public export FromVar Dim where fromVarLoc = B
+public export FromVar Dim where fromVar = B
 
 
 export

lib/Quox/Syntax/DimEq.idr

@@ -70,13 +70,13 @@ toMaybe (Just x) = Just x
 
 
 export
-fromGround' : Context' DimConst d -> DimEq' d
+fromGround' : BContext d -> Context' DimConst d -> DimEq' d
-fromGround' [<]        = [<]
+fromGround' [<]       [<]        = [<]
-fromGround' (ctx :< e) = fromGround' ctx :< Just (K e noLoc)
+fromGround' (xs :< x) (ctx :< e) = fromGround' xs ctx :< Just (K e x.loc)
 
 export
-fromGround : Context' DimConst d -> DimEq d
+fromGround : BContext d -> Context' DimConst d -> DimEq d
-fromGround = C . fromGround'
+fromGround = C .: fromGround'
 
 
 public export %inline
@@ -243,7 +243,7 @@ prettyCsts : {opts : _} -> BContext d -> DimEq' d ->
 prettyCsts [<] [<] = pure [<]
 prettyCsts dnames (eqs :< Nothing) = prettyCsts (tail dnames) eqs
 prettyCsts dnames (eqs :< Just q)  =
-  [|prettyCsts (tail dnames) eqs :< prettyCst dnames (BV 0 noLoc) (weakD 1 q)|]
+  [|prettyCsts (tail dnames) eqs :< prettyCst dnames (BV 0 q.loc) (weakD 1 q)|]
 
 export
 prettyDimEq' : {opts : _} -> BContext d -> DimEq' d -> Eff Pretty (Doc opts)

lib/Quox/Syntax/Subst.idr

@@ -49,7 +49,7 @@ interface FromVar term => CanSubstSelf term where
 
 public export
 getLoc : FromVar term => Subst term from to -> Var from -> Loc -> term to
-getLoc (Shift by) i      loc = fromVarLoc (shift by i) loc
+getLoc (Shift by) i      loc = fromVar (shift by i) loc
 getLoc (t ::: th) VZ     _   = t
 getLoc (t ::: th) (VS i) loc = getLoc th i loc
 
@@ -95,18 +95,18 @@ map f (t ::: th) = f t ::: map f th
 
 
 public export %inline
-push : CanSubstSelf f => Subst f from to -> Subst f (S from) (S to)
+push : CanSubstSelf f => Subst f from to -> Loc -> Subst f (S from) (S to)
-push th = fromVar VZ ::: (th . shift 1)
+push th loc = fromVar VZ loc ::: (th . shift 1)
 
 -- [fixme] a better way to do this?
 public export
 pushN : CanSubstSelf f => (s : Nat) ->
-        Subst f from to -> Subst f (s + from) (s + to)
+        Subst f from to -> Loc -> Subst f (s + from) (s + to)
-pushN 0     th = th
+pushN 0     th _   = th
-pushN (S s) th =
+pushN (S s) th loc =
   rewrite plusSuccRightSucc s from in
   rewrite plusSuccRightSucc s to in
-  pushN s $ fromVar VZ ::: (th . shift 1)
+  pushN s (fromVar VZ loc ::: (th . shift 1)) loc
 
 public export
 drop1 : Subst f (S from) to -> Subst f from to

lib/Quox/Syntax/Term/Base.idr

@@ -102,6 +102,16 @@ mutual
     ||| pair value
     Pair : (fst, snd : Term d n) -> (loc : Loc) -> Term d n
 
+    ||| inductive (w) type `(x : A) ⊲ B`
+    W : (shape : Term d n) ->
+        (body : ScopeTerm d n) -> (loc : Loc) -> Term d n
+    ||| subterms for `(x : A) ⊲ B` are:
+    |||   1. `x : A`
+    |||      (the "constructor" and non-recursive fields)
+    |||   2. `f : 1.(B x) → (x : A) ⊲ B`
+    |||      (the recursive fields, one for each element of B x)
+    Sup : (root, sub : Term d n) -> (loc : Loc) -> Term d n
+
     ||| enumeration type
     Enum : (cases : SortedSet TagVal) -> (loc : Loc) -> Term d n
     ||| enumeration value
@@ -155,6 +165,13 @@ mutual
                (loc : Loc) ->
                Elim d n
 
+    ||| recursion
+    CaseW : (qty, qtyIH : Qty) -> (tree : Elim d n) ->
+            (ret : ScopeTerm d n) ->
+            (body : ScopeTermN 3 d n) ->
+            (loc : Loc) ->
+            Elim d n
+
     ||| enum matching
     CaseEnum : (qty : Qty) -> (tag : Elim d n) ->
                (ret : ScopeTerm d n) ->
@@ -344,6 +361,11 @@ public export %inline
 enum : List TagVal -> Loc -> Term d n
 enum ts loc = Enum (SortedSet.fromList ts) loc
 
+public export %inline
+caseEnum : Qty -> Elim d n -> ScopeTerm d n -> List (TagVal, Term d n) -> Loc ->
+           Elim d n
+caseEnum q e ret arms loc = CaseEnum q e ret (SortedMap.fromList arms) loc
+
 public export %inline
 typeCase : Elim d n -> Term d n ->
            List (TypeCaseArm d n) -> Term d n -> Loc -> Elim d n
@@ -364,6 +386,7 @@ Located (Elim d n) where
   (B _ loc).loc                 = loc
   (App _ _ loc).loc             = loc
   (CasePair _ _ _ _ loc).loc    = loc
+  (CaseW _ _ _ _ _ loc).loc     = loc
   (CaseEnum _ _ _ _ loc).loc    = loc
   (CaseNat _ _ _ _ _ _ loc).loc = loc
   (CaseBox _ _ _ _ loc).loc     = loc
@@ -382,6 +405,8 @@ Located (Term d n) where
   (Lam _ loc).loc       = loc
   (Sig _ _ loc).loc     = loc
   (Pair _ _ loc).loc    = loc
+  (W _ _ loc).loc       = loc
+  (Sup _ _ loc).loc     = loc
   (Enum _ loc).loc      = loc
   (Tag _ loc).loc       = loc
   (Eq _ _ _ loc).loc    = loc
@@ -412,6 +437,8 @@ Relocatable (Elim d n) where
   setLoc loc (App fun arg _) = App fun arg loc
   setLoc loc (CasePair qty pair ret body _) =
     CasePair qty pair ret body loc
+  setLoc loc (CaseW qty qtyIH tree ret body _) =
+    CaseW qty qtyIH tree ret body loc
   setLoc loc (CaseEnum qty tag ret arms _) =
     CaseEnum qty tag ret arms loc
   setLoc loc (CaseNat qty qtyIH nat ret zero succ _) =
@@ -440,6 +467,8 @@ Relocatable (Term d n) where
   setLoc loc (Lam body _) = Lam body loc
   setLoc loc (Sig fst snd _) = Sig fst snd loc
   setLoc loc (Pair fst snd _) = Pair fst snd loc
+  setLoc loc (W shape body _) = W shape body loc
+  setLoc loc (Sup root sub _) = Sup root sub loc
   setLoc loc (Enum cases _) = Enum cases loc
   setLoc loc (Tag tag _) = Tag tag loc
   setLoc loc (Eq ty l r _) = Eq ty l r loc

lib/Quox/Syntax/Term/Pretty.idr

@@ -346,6 +346,8 @@ prettyTyCasePat KPi [< a, b] =
   parens . hsep =<< sequence [prettyTBind a, arrowD, prettyTBind b]
 prettyTyCasePat KSig [< a, b] =
   parens . hsep =<< sequence [prettyTBind a, timesD, prettyTBind b]
+prettyTyCasePat KW [< a, b] =
+  parens . hsep =<< sequence [prettyTBind a, triD, prettyTBind b]
 prettyTyCasePat KEnum [<] = hl Syntax $ text "{}"
 prettyTyCasePat KEq [< a0, a1, a, l, r] =
   hsep <$> sequence (eqD :: map prettyTBind [a0, a1, a, l, r])
@@ -420,6 +422,21 @@ prettyTerm dnames tnames p@(Pair fst snd _) =
       withPrec Outer $ prettyTerm dnames tnames $ assert_smaller p t
     pure $ separateTight !commaD lines
 
+prettyTerm dnames tnames (W a b _) = do
+  parensIfM W =<< do
+    left <- prettySigBind1 b.name dnames tnames a
+    right <- withPrec InW $
+             prettyTerm dnames (tnames :< b.name) (assert_smaller b b.term)
+    pure $ sep [hsep [left, !triD], right]
+
+prettyTerm dnames tnames (Sup root sub _) = do
+  parensIfM Sup =<< do
+    left  <- withPrec InSup $ prettyTerm dnames tnames root
+    right <- withPrec InSup $ prettyTerm dnames tnames sub
+    pure $
+      hsep [left, !diamondD, right] <|>
+      vsep [hsep [left, !diamondD], !(indentD right)]
+
 prettyTerm dnames tnames (Enum cases _) =
   prettyEnum $ SortedSet.toList cases
 
@@ -446,17 +463,22 @@ prettyTerm dnames tnames s@(DLam {}) =
 prettyTerm dnames tnames (Nat _) = natD
 prettyTerm dnames tnames (Zero _) = hl Syntax "0"
 prettyTerm dnames tnames (Succ p _) = do
-  succD <- succD
+  s <- succD
-  let succ : Doc opts -> Eff Pretty (Doc opts)
+  either (succ s) prettyNat =<< tryToNat s p
-      succ t = prettyAppD succD [t]
+where
-      toNat : Term d n -> Eff Pretty (Either (Doc opts) Nat)
+  succ : Doc opts -> Doc opts -> Eff Pretty (Doc opts)
-      toNat s with (pushSubsts' s)
+  succ s t = prettyAppD s [t]
+
+  tryToNat : Doc opts -> Term d n -> Eff Pretty (Either (Doc opts) Nat)
+  tryToNat s t with (pushSubsts' t)
     _ | Zero _   = pure $ Right 0
-        _ | Succ d _ = bitraverse succ (pure . S) =<<
+    _ | Succ d _ = bitraverse (succ s) (pure . S) =<<
-                       toNat (assert_smaller s d)
+                   tryToNat s (assert_smaller t d)
-        _ | s'       = map Left . withPrec Arg $
+    _ | t'       = map Left . withPrec Arg $
-                       prettyTerm dnames tnames $ assert_smaller s s'
+                   prettyTerm dnames tnames $ assert_smaller t t'
-  either succ (hl Syntax . text . show . S) =<< toNat p
+
+  prettyNat : Nat -> Eff Pretty (Doc opts)
+  prettyNat = hl Syntax . text . show . S
 
 prettyTerm dnames tnames (BOX qty ty _) =
   bracks . hcat =<<
@@ -493,6 +515,16 @@ prettyElim dnames tnames (CasePair qty pair ret body _) = do
   prettyCase dnames tnames qty pair ret
     [MkCaseArm pat [<] [< x, y] body.term]
 
+prettyElim dnames tnames (CaseW qty qtyIH tree ret body _) = do
+  let [< t, r, ih] = body.names
+  pat0 <- hsep <$> sequence [prettyTBind t, diamondD, prettyTBind r]
+  ihpat <- map hcat $ sequence [prettyQty qtyIH, dotD, prettyTBind ih]
+  pat <- if ih.name == Unused
+         then pure pat0
+         else pure $ hsep [pat0 <+> !commaD, ihpat]
+  let arm = MkCaseArm pat [<] [< t, r, ih] body.term
+  prettyCase dnames tnames qty tree ret [arm]
+
 prettyElim dnames tnames (CaseEnum qty tag ret arms _) = do
   arms <- for (SortedMap.toList arms) $ \(tag, body) =>
     pure $ MkCaseArm !(prettyTag tag) [<] [<] body

lib/Quox/Syntax/Term/Subst.idr

@@ -56,12 +56,12 @@ namespace DSubst.DScopeTermN
   (//) : {s : Nat} ->
          DScopeTermN s d1 n -> Lazy (DSubst d1 d2) ->
          DScopeTermN s d2 n
-  S ns (Y body) // th = S ns $ Y $ body // pushN s th
+  S ns (Y body) // th = S ns $ Y $ body // pushN s th body.loc
   S ns (N body) // th = S ns $ N $ body // th
 
 
-export %inline FromVar (Elim d) where fromVarLoc = B
+export %inline FromVar (Elim d) where fromVar = B
-export %inline FromVar (Term d) where fromVarLoc = E .: fromVar
+export %inline FromVar (Term d) where fromVar = E .: fromVar
 
 
 ||| does the minimal reasonable work:
@@ -104,7 +104,7 @@ namespace ScopeTermN
   (//) : {s : Nat} ->
          ScopeTermN s d n1 -> Lazy (TSubst d n1 n2) ->
          ScopeTermN s d n2
-  S ns (Y body) // th = S ns $ Y $ body // pushN s th
+  S ns (Y body) // th = S ns $ Y $ body // pushN s th body.loc
   S ns (N body) // th = S ns $ N $ body // th
 
 namespace DScopeTermN
@@ -147,24 +147,24 @@ weakE by t = t // shift by
 
 parameters {s : Nat}
   namespace ScopeTermBody
-    export %inline
+    public export %inline
     (.term) : ScopedBody s (Term d) n -> Term d (s + n)
     (Y b).term = b
     (N b).term = weakT s b
 
   namespace ScopeTermN
-    export %inline
+    public export %inline
     (.term) : ScopeTermN s d n -> Term d (s + n)
     t.term = t.body.term
 
   namespace DScopeTermBody
-    export %inline
+    public export %inline
     (.term) : ScopedBody s (\d => Term d n) d -> Term (s + d) n
     (Y b).term = b
     (N b).term = dweakT s b
 
   namespace DScopeTermN
-    export %inline
+    public export %inline
     (.term) : DScopeTermN s d n -> Term (s + d) n
     t.term = t.body.term
 
@@ -189,12 +189,12 @@ dsub1 t p = dsubN t [< p]
 
 
 public export %inline
-(.zero) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
+(.zero) : DScopeTerm d n -> Term d n
-body.zero = dsub1 body $ K Zero loc
+body.zero = dsub1 body $ K Zero body.loc
 
 public export %inline
-(.one) : DScopeTerm d n -> {default noLoc loc : Loc} -> Term d n
+(.one) : DScopeTerm d n -> Term d n
-body.one = dsub1 body $ K One loc
+body.one = dsub1 body $ K One body.loc
 
 
 public export
@@ -261,6 +261,10 @@ mutual
       nclo $ Sig (a // th // ph) (b // th // ph) loc
     pushSubstsWith th ph (Pair s t loc) =
       nclo $ Pair (s // th // ph) (t // th // ph) loc
+    pushSubstsWith th ph (W a b loc) =
+      nclo $ W (a // th // ph) (b // th // ph) loc
+    pushSubstsWith th ph (Sup s t loc) =
+      nclo $ Sup (s // th // ph) (t // th // ph) loc
     pushSubstsWith th ph (Enum tags loc) =
       nclo $ Enum tags loc
     pushSubstsWith th ph (Tag tag loc) =
@@ -299,6 +303,8 @@ mutual
       nclo $ App (f // th // ph) (s // th // ph) loc
     pushSubstsWith th ph (CasePair pi p r b loc) =
       nclo $ CasePair pi (p // th // ph) (r // th // ph) (b // th // ph) loc
+    pushSubstsWith th ph (CaseW pi pi' e r b loc) =
+      nclo $ CaseW pi pi' (e // th // ph) (r // th // ph) (b // th // ph) loc
     pushSubstsWith th ph (CaseEnum pi t r arms loc) =
       nclo $ CaseEnum pi (t // th // ph) (r // th // ph)
                (map (\b => b // th // ph) arms) loc

lib/Quox/Syntax/Term/Tighten.idr

@@ -52,6 +52,10 @@ mutual
     Sig <$> tightenT p fst <*> tightenS p snd <*> pure loc
   tightenT' p (Pair fst snd loc) =
     Pair <$> tightenT p fst <*> tightenT p snd <*> pure loc
+  tightenT' p (W shape body loc) =
+    W <$> tightenT p shape <*> tightenS p body <*> pure loc
+  tightenT' p (Sup root sub loc) =
+    Sup <$> tightenT p root <*> tightenT p sub <*> pure loc
   tightenT' p (Enum cases loc) =
     pure $ Enum cases loc
   tightenT' p (Tag tag loc) =
@@ -87,6 +91,12 @@ mutual
                  <*> tightenS p ret
                  <*> tightenS p body
                  <*> pure loc
+  tightenE' p (CaseW qty qtyIH tree ret body loc) =
+    CaseW qty qtyIH
+      <$> tightenE p tree
+      <*> tightenS p ret
+      <*> tightenS p body
+      <*> pure loc
   tightenE' p (CaseEnum qty tag ret arms loc) =
     CaseEnum qty <$> tightenE p tag
                  <*> tightenS p ret
@@ -167,6 +177,10 @@ mutual
     Sig <$> dtightenT p fst <*> dtightenS p snd <*> pure loc
   dtightenT' p (Pair fst snd loc) =
     Pair <$> dtightenT p fst <*> dtightenT p snd <*> pure loc
+  dtightenT' p (W shape body loc) =
+    W <$> dtightenT p shape <*> dtightenS p body <*> pure loc
+  dtightenT' p (Sup root sub loc) =
+    Sup <$> dtightenT p root <*> dtightenT p sub <*> pure loc
   dtightenT' p (Enum cases loc) =
     pure $ Enum cases loc
   dtightenT' p (Tag tag loc) =
@@ -202,6 +216,12 @@ mutual
                  <*> dtightenS p ret
                  <*> dtightenS p body
                  <*> pure loc
+  dtightenE' p (CaseW qty qtyIH tree ret body loc) =
+    CaseW qty qtyIH
+      <$> dtightenE p tree
+      <*> dtightenS p ret
+      <*> dtightenS p body
+      <*> pure loc
   dtightenE' p (CaseEnum qty tag ret arms loc) =
     CaseEnum qty <$> dtightenE p tag
                  <*> dtightenS p ret

lib/Quox/Syntax/Term/TyConKind.idr

@@ -9,7 +9,7 @@ import Generics.Derive
 
 
 public export
-data TyConKind = KTYPE | KPi | KSig | KEnum | KEq | KNat | KBOX
+data TyConKind = KTYPE | KPi | KSig | KW | KEnum | KEq | KNat | KBOX
 %name TyConKind k
 %runElab derive "TyConKind" [Eq.Eq, Ord.Ord, Show.Show, Generic, Meta, DecEq]
 
@@ -28,6 +28,7 @@ arity : TyConKind -> Nat
 arity KTYPE = 0
 arity KPi   = 2
 arity KSig  = 2
+arity KW    = 2
 arity KEnum = 0
 arity KEq   = 5
 arity KNat  = 0

lib/Quox/Syntax/Var.idr

@@ -139,13 +139,9 @@ weakIsSpec p i = toNatInj $ trans (weakCorrect p i) (sym $ weakSpecCorrect p i)
 
 
 public export
-interface FromVar f where %inline fromVarLoc : Var n -> Loc -> f n
+interface FromVar f where %inline fromVar : Var n -> Loc -> f n
 
-public export %inline
+public export FromVar Var where fromVar x _ = x
-fromVar : FromVar f => Var n -> {default noLoc loc : Loc} -> f n
-fromVar x = fromVarLoc x loc
-
-public export FromVar Var where fromVarLoc x _ = x
 
 export
 tabulateV : {0 tm : Nat -> Type} -> (forall n. Var n -> tm n) ->

lib/Quox/Typechecker.idr

@@ -57,27 +57,40 @@ typecaseTel : (k : TyConKind) -> BContext (arity k) -> Universe ->
               CtxExtension d n (arity k + n)
 typecaseTel k xs u = case k of
   KTYPE => [<]
-  -- A : ★ᵤ, B : 0.A → ★ᵤ
+  KPi   => binaryTyCon xs
-  KPi =>
+  KSig  => binaryTyCon xs
-    let [< a, b] = xs in
+  KW    => binaryTyCon xs
-    [< (Zero, a, TYPE u a.loc),
-       (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
-  KSig =>
-    let [< a, b] = xs in
-    [< (Zero, a, TYPE u a.loc),
-       (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
   KEnum => [<]
-  -- A₀ : ★ᵤ, A₁ : ★ᵤ, A : (A₀ ≡ A₁ : ★ᵤ), L : A₀, R : A₀
+  KEq   => eqCon xs
-  KEq =>
+  KNat  => [<]
-    let [< a0, a1, a, l, r] = xs in
+  KBOX  => unaryTyCon xs
+where
+  -- 0.A : ★ᵤ
+  unaryTyCon : BContext 1 -> CtxExtension d n (S n)
+  unaryTyCon [< a] = [< (Zero, a, TYPE u a.loc)]
+
+  -- 0.A : ★ᵤ, 0.B : 0.A → ★ᵤ
+  binaryTyCon : BContext 2 -> CtxExtension d n (2 + n)
+  binaryTyCon [< a, b] =
+    [< (Zero, a, TYPE u a.loc),
+       (Zero, b, Arr Zero (BVT 0 b.loc) (TYPE u b.loc) b.loc)]
+
+  -- 0.A₀ : ★ᵤ, 0.A₁ : ★ᵤ, 0.A : (A₀ ≡ A₁ : ★ᵤ), 0.L : A₀, 0.R : A₁
+  eqCon : BContext 5 -> CtxExtension d n (5 + n)
+  eqCon [< a0, a1, a, l, r] =
     [< (Zero, a0, TYPE u a0.loc),
        (Zero, a1, TYPE u a1.loc),
        (Zero, a,  Eq0 (TYPE u a.loc) (BVT 1 a.loc) (BVT 0 a.loc) a.loc),
        (Zero, l,  BVT 2 l.loc),
        (Zero, r,  BVT 2 r.loc)]
-  KNat => [<]
+
-  -- A : ★ᵤ
+||| if a ⋄ b : (x : A) ⊲ B, then b : `supSubTy a A B _`
-  KBOX => let [< a] = xs in [< (Zero, a, TYPE u a.loc)]
+||| i.e. ω.B[a∷A/x] → ((x : A) ⊲ B)
+export
+supSubTy : (root, rootTy : Term d n) ->
+           (body : ScopeTerm d n) -> Loc -> Term d n
+supSubTy root rootTy body loc =
+  Arr Any (sub1 body (Ann root rootTy root.loc)) (W rootTy body loc) loc
 
 
 mutual
@@ -188,6 +201,17 @@ mutual
 
   check' ctx sg t@(Sig {}) ty = toCheckType ctx sg t ty
 
+  check' ctx sg t@(W {}) ty = toCheckType ctx sg t ty
+
+  check' ctx sg (Sup root sub loc) ty = do
+    (shape, body) <- expectW !(askAt DEFS) ctx ty.loc ty
+    -- if Ψ | Γ ⊢ σ · a ⇐ A ⊳ Σ₁
+    qroot <- checkC ctx sg root shape
+    -- if Ψ | Γ ⊢ σ · b ⇐ ω.B[a∷A/x] → ((x : A) ⊲ B) ⊳ Σ₂
+    qsub <- checkC ctx sg sub (supSubTy root shape body sub.loc)
+    -- then Ψ | Γ ⊢ σ · (a ⋄ b) ⇐ ((x : A) ⊲ B) ⊳ Σ₁+ωΣ₂
+    pure $ qroot + Any * qsub
+
   check' ctx sg (Pair fst snd loc) ty = do
     (tfst, tsnd) <- expectSig !(askAt DEFS) ctx ty.loc ty
     -- if Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ₁
@@ -281,6 +305,16 @@ mutual
   checkType' ctx t@(Pair {}) u =
     throw $ NotType t.loc ctx t
 
+  checkType' ctx (W shape body _) u = do
+    -- if Ψ | Γ ⊢₀ A ⇐ Type ℓ
+    checkTypeC ctx shape u
+    -- if Ψ | Γ, x : A ⊢₀ B ⇐ Type ℓ
+    checkTypeScope ctx shape body u
+    -- then Ψ | Γ ⊢₀ (x : A) ⊲ π.B ⇐ Type ℓ
+
+  checkType' ctx t@(Sup {}) u =
+    throw $ NotType t.loc ctx t
+
   checkType' ctx (Enum {}) u = pure ()
     -- Ψ | Γ ⊢₀ {ts} ⇐ Type ℓ
 
@@ -313,7 +347,7 @@ mutual
     infres <- inferC ctx szero e
     -- if Ψ | Γ ⊢ Type ℓ <: Type 𝓀
     case u of
-      Just u  => lift $ subtype e.loc ctx infres.type (TYPE u noLoc)
+      Just u  => lift $ subtype e.loc ctx infres.type (TYPE u e.loc)
       Nothing => ignore $ expectTYPE !(askAt DEFS) ctx e.loc infres.type
     -- then Ψ | Γ ⊢₀ E ⇐ Type 𝓀
 
@@ -388,6 +422,42 @@ mutual
       qout = pi * pairres.qout + bodyout
     }
 
+  infer' ctx sg (CaseW pi si tree ret body loc) = do
+    -- if 1 ≤ π
+    expectCompatQ loc One pi
+    -- if Ψ | Γ ⊢ σ · e ⇒ ((x : A) ⊲ B) ⊳ Σ₁
+    InfRes {type = w, qout = qtree} <- inferC ctx sg tree
+    -- if Ψ | Γ, p : (x : A) ⊲ B ⊢₀ C ⇐ Type
+    checkTypeC (extendTy Zero ret.name w ctx) ret.term Nothing
+    (shape, tbody) <- expectW !(askAt DEFS) ctx tree.loc w
+    -- if Ψ | Γ, x : A, y : ω.B → (x : A) ⊲ B,
+    --           ih : π.(z : B) → C[y z/p]
+    --  ⊢ σ · u ⇐ C[((x ⋄ y) ∷ (x : A) ⊲ B)/p]
+    --  ⊳ Σ₂, π'.x, ς₁.y, ς₂.ih
+    -- with π' ≤ σπ,  ς₂ ≤ σς,  ς₁+ς₂ ≤ σπ
+    let [< x, y, ih] = body.names
+        -- ω.B → (x : A) ⊲ B
+        tsub = Arr Any tbody.term (weakT 1 w) y.loc
+        -- y z
+        ihret = App (BV 1 y.loc) (BVT 0 ih.loc) y.loc
+        -- π.(z : B) → C[y z/p]
+        tih  = PiY pi !(mnb "z" ih.loc)
+                   (tbody.term // (BV 1 x.loc ::: shift 2))
+                   (ret.term // (ihret ::: shift 3)) ih.loc
+        sp = sg.fst * pi; ss = sg.fst * si
+        ctx' = extendTyN [< (sp, x, shape), (sp, y, tsub), (ss, ih, tih)] ctx
+    qbody' <- checkC ctx' sg body.term $ substCaseWRet body.names w ret
+    let qbody :< qx :< qy :< qih = qbody'
+    expectCompatQ x.loc qx sp
+    expectCompatQ (ih.loc `or` loc) qih ss
+    expectCompatQ y.loc (qy + qih) sp -- [todo] better error message
+    -- then Ψ | Γ ⊢ σ · caseπ e return p ⇒ C of { x ⋄ y, ς.ih ⇒ u }
+    --            ⇒ C[e/p] ⊳ Σ₁+Σ₂
+    pure $ InfRes {
+      type = sub1 ret tree,
+      qout = qtree + qbody
+    }
+
   infer' ctx sg (CaseEnum pi t ret arms loc) {d, n} = do
     -- if Ψ | Γ ⊢ σ · t ⇒ {ts} ⊳ Σ₁
     tres <- inferC ctx sg t

lib/Quox/Typing.idr

@@ -47,14 +47,22 @@ public export
 substCasePairRet : BContext 2 -> Term d n -> ScopeTerm d n -> Term d (2 + n)
 substCasePairRet [< x, y] dty retty =
   let tm = Pair (BVT 1 x.loc) (BVT 0 y.loc) $ x.loc `extendL` y.loc
-      arg = Ann tm (dty // fromNat 2) tm.loc
+      arg = Ann tm (dty // shift 2) tm.loc
   in
   retty.term // (arg ::: shift 2)
 
+public export
+substCaseWRet : BContext 3 -> Term d n -> ScopeTerm d n -> Term d (3 + n)
+substCaseWRet [< x, y, ih] dty retty =
+  let tm = Sup (BVT 2 x.loc) (BVT 1 y.loc) $ x.loc `extendL` y.loc
+      arg = Ann tm (dty // shift 3) tm.loc
+  in
+  sub1 (weakS 3 retty) arg
+
 public export
 substCaseSuccRet : BContext 2 -> ScopeTerm d n -> Term d (2 + n)
 substCaseSuccRet [< p, ih] retty =
-  let arg = Ann (Succ (BVT 1 p.loc) p.loc) (Nat noLoc) $ p.loc `extendL` ih.loc
+  let arg = Ann (Succ (BVT 1 p.loc) p.loc) (Nat p.loc) $ p.loc `extendL` ih.loc
   in
   retty.term // (arg ::: shift 2)
 
@@ -95,6 +103,10 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
     expectSig : Term d n -> Eff fs (Term d n, ScopeTerm d n)
     expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
 
+    export covering %inline
+    expectW : Term d n -> Eff fs (Term d n, ScopeTerm d n)
+    expectW = expect ExpectedW `(W {shape, body, _}) `((shape, body))
+
     export covering %inline
     expectEnum : Term d n -> Eff fs (SortedSet TagVal)
     expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)
@@ -143,6 +155,10 @@ parameters (defs : Definitions) {auto _ : (Has ErrorEff fs, Has NameGen fs)}
     expectSig : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n)
     expectSig = expect ExpectedSig `(Sig {fst, snd, _}) `((fst, snd))
 
+    export covering %inline
+    expectW : Term 0 n -> Eff fs (Term 0 n, ScopeTerm 0 n)
+    expectW = expect ExpectedW `(W {shape, body, _}) `((shape, body))
+
     export covering %inline
     expectEnum : Term 0 n -> Eff fs (SortedSet TagVal)
     expectEnum = expect ExpectedEnum `(Enum {cases, _}) `(cases)

lib/Quox/Typing/Context.idr

@@ -197,7 +197,7 @@ namespace EqContext
   toTyContext : (e : EqContext n) -> TyContext e.dimLen n
   toTyContext (MkEqContext {dimLen, dassign, dnames, tctx, tnames, qtys}) =
     MkTyContext {
-      dctx = fromGround dassign,
+      dctx = fromGround dnames dassign,
       tctx = map (// shift0 dimLen) tctx,
       dnames, tnames, qtys
     }

lib/Quox/Typing/Error.idr

@@ -58,6 +58,7 @@ data Error
 = ExpectedTYPE Loc (NameContexts d n) (Term d n)
 | ExpectedPi   Loc (NameContexts d n) (Term d n)
 | ExpectedSig  Loc (NameContexts d n) (Term d n)
+| ExpectedW    Loc (NameContexts d n) (Term d n)
 | ExpectedEnum Loc (NameContexts d n) (Term d n)
 | ExpectedEq   Loc (NameContexts d n) (Term d n)
 | ExpectedNat  Loc (NameContexts d n) (Term d n)
@@ -116,6 +117,7 @@ Located Error where
   (ExpectedTYPE    loc _ _).loc       = loc
   (ExpectedPi      loc _ _).loc       = loc
   (ExpectedSig     loc _ _).loc       = loc
+  (ExpectedW       loc _ _).loc       = loc
   (ExpectedEnum    loc _ _).loc       = loc
   (ExpectedEq      loc _ _).loc       = loc
   (ExpectedNat     loc _ _).loc       = loc
@@ -256,12 +258,16 @@ prettyErrorNoLoc showContext = \case
     hangDSingle "expected a pair type, but got"
       !(prettyTerm ctx.dnames ctx.tnames s)
 
+  ExpectedW _ ctx s =>
+    hangDSingle "expected an inductive (W) type, but got"
+      !(prettyTerm ctx.dnames ctx.tnames s)
+
   ExpectedEnum _ ctx s =>
     hangDSingle "expected an enumeration type, but got"
       !(prettyTerm ctx.dnames ctx.tnames s)
 
   ExpectedEq _ ctx s =>
-    hangDSingle "expected an enumeration type, but got"
+    hangDSingle "expected an equality type, but got"
       !(prettyTerm ctx.dnames ctx.tnames s)
 
   ExpectedNat _ ctx s =>

syntax.ebnf

@@ -24,7 +24,7 @@ dim arg = "@", dim.
 
 pat var = NAME | "_".
 
-term = lambda | case | pi | sigma | ann.
+term = lambda | case | pi | w | sigma | ann.
 
 lambda = ("λ" | "δ"), {pat var}+, "⇒", term.
 
@@ -39,17 +39,22 @@ pattern = "zero" | "0"
             (* default qty for IH is 1 *)
         | TAG
         | "[", pat var, "]"
-        | "(", pat var, ",", pat var, ")".
+        | "(", pat var, ",", pat var, ")"
+        | pat var, "⋄", pat var, [",", [qty, "."], pat var].
 
 (* default qty is 1 *)
 pi = [qty, "."], (binder | term arg), "→", term.
 binder = "(", {NAME}+, ":", term, ")".
 
+w = binder, "⊲", ann.
+
 sigma = (binder | ann), "×", (sigma | ann).
 
 ann = infix eq, ["∷", term].
 
-infix eq = app term, ["≡", term, ":", app term]. (* dependent is below *)
+infix eq = sup term, ["≡", term, ":", sup term]. (* dependent is below *)
+
+sup term = app term, ["⋄", app term].
 
 app term       = coe | comp | split universe | dep eq | succ | normal app.
 split universe = "★", NAT.

tests/Tests/DimEq.idr

@@ -97,7 +97,7 @@ tests = "dimension constraints" :- [
     testPrettyD iijj ZeroIsOne "𝑖, 𝑗, 0 = 1",
     testPrettyD [<] new "" {label = "[empty output from empty context]"},
     testPrettyD ii new "𝑖",
-    testPrettyD iijj (fromGround [< Zero, One])
+    testPrettyD iijj (fromGround iijj [< Zero, One])
       "𝑖, 𝑗, 𝑖 = 0, 𝑗 = 1",
     testPrettyD iijj (C [< Just (^K Zero), Nothing])
       "𝑖, 𝑗, 𝑖 = 0",

tests/Tests/Equal.idr

@@ -16,6 +16,8 @@ defGlobals = fromList
    ("a'", ^mkPostulate gany (^FT "A" 0)),
    ("b", ^mkPostulate gany (^FT "B" 0)),
    ("f", ^mkPostulate gany (^Arr One (^FT "A" 0) (^FT "A" 0))),
+   ("absurd", ^mkDef gany (^Arr One (^enum []) (^FT "A" 0))
+      (^LamY "v" (E $ ^caseEnum One (^BV 0) (SN $ ^FT "A" 0) []))),
    ("id", ^mkDef gany (^Arr One (^FT "A" 0) (^FT "A" 0)) (^LamY "x" (^BVT 0))),
    ("eq-AB", ^mkPostulate gzero (^Eq0 (^TYPE 0) (^FT "A" 0) (^FT "B" 0))),
    ("two", ^mkDef gany (^Nat) (^Succ (^Succ (^Zero))))]
@@ -517,6 +519,18 @@ tests = "equality & subtyping" :- [
 
   todo "pair elim",
 
+  todo "w types",
+
+  "sup" :- [
+    testEq "a ⋄ absurd ≡ a ⋄ absurd : A ⊲ {}" $
+      equalT empty
+        (^W (^FT "A" 0) (SN $ ^enum []))
+        (^Sup (^FT "a" 0) (^FT "absurd" 0))
+        (^Sup (^FT "a" 0) (^FT "absurd" 0))
+  ],
+
+  todo "w elim",
+
   todo "enum types",
   todo "enum",
   todo "enum elim",

tests/Tests/Parser.idr

@@ -168,6 +168,8 @@ tests = "parser" :- [
           (App (V "B" {}) (V "x" {}) _) _) _),
     parseMatch term "(x : A) → B x"
       `(Pi (PQ One _) (PV "x" _) (V "A" {}) (App (V "B" {}) (V "x" {}) _) _),
+    parseFails term "(x : A) → (y : B x)",
+    parseFails term "(x : A) → 1.(B x)",
     parseMatch term "1.A → B"
       `(Pi (PQ One _) (Unused _) (V "A" {}) (V "B" {}) _),
     parseMatch term "A → B"
@@ -249,6 +251,43 @@ tests = "parser" :- [
     parseFails term "(x,,y)"
   ],
 
+  "w" :- [
+    parseMatch term "(x : A) ⊲ B"
+      `(W (PV "x" _) (V "A" {}) (V "B" {}) _),
+    parseFails term "(x y : A) ⊲ B",
+    parseFails term "1.(x : A) ⊲ B",
+    parseMatch term "(x : A) ⊲ (y : B) ⊲ C"
+      `(W (PV "x" _) (V "A" {})
+        (W (PV "y" _) (V "B" {})  (V "C" {}) _) _),
+    parseMatch term "A ⊲ B"
+      `(W _ (V "A" {}) (V "B" {}) _),
+    parseMatch term "A <| B"
+      `(W _ (V "A" {}) (V "B" {}) _),
+    parseFails term "A ⊲ (y : B)",
+    parseMatch term "(x : A) ⊲ B x × C"
+      `(W (PV "x" _) (V "A" {})
+         (Sig _ (App (V "B" {}) (V "x" {}) _) (V "C" {}) _) _),
+    parseMatch term "A ⊲ B → C"
+      `(Pi _ _ (W _ (V "A" {}) (V "B" {}) _) (V "C" {}) _),
+    parseMatch term "A → B ⊲ C"
+      `(Pi _ _ (V "A" {}) (W _ (V "B" {}) (V "C" {}) _) _)
+  ],
+
+  "sup" :- [
+    parseMatch term "s ⋄ t"
+      `(Sup (V "s" {}) (V "t" {}) _),
+    parseMatch term "s ⋄ t ⋄ u"
+      `(Sup (V "s" {}) (Sup (V "t" {}) (V "u" {}) _) _),
+    parseMatch term "s <> t"
+      `(Sup (V "s" {}) (V "t" {}) _),
+    parseMatch term "a b ⋄ c d"
+      `(Sup (App (V "a" {}) (V "b" {}) _) (App (V "c" {}) (V "d" {}) _) _),
+    parseMatch term "a ⋄ b ≡ a' ⋄ b' : (A ⊲ B)"
+      `(Eq (_, W _ (V "A" {}) (V "B" {}) _)
+           (Sup (V "a"  {}) (V "b"  {}) _)
+           (Sup (V "a'" {}) (V "b'" {}) _) _)
+  ],
+
   "equality type" :- [
     parseMatch term "Eq (i ⇒ A) s t"
       `(Eq (PV "i" _, V "A" {}) (V "s" {}) (V "t" {}) _),
@@ -396,8 +435,23 @@ tests = "parser" :- [
     parseMatch term "caseω n return ℕ of { succ _, ih ⇒ ih; zero ⇒ 0; }"
       `(Case (PQ Any _) (V "n" {}) (Unused _, Nat _)
         (CaseNat (Zero _) (Unused _, PQ One _, PV "ih" _, V "ih" {}) _) _),
+    parseMatch term "caseω n return ℕ of { succ _, _ ⇒ ih; zero ⇒ 0; }"
+      `(Case (PQ Any _) (V "n" {}) (Unused _, Nat _)
+        (CaseNat (Zero _) (Unused _, PQ Zero _, Unused _, V "ih" {}) _) _),
     parseFails term "caseω n return A of { zero ⇒ a }",
-    parseFails term "caseω n return ℕ of { succ ⇒ 5 }"
+    parseFails term "caseω n return ℕ of { succ ⇒ 5 }",
+    parseMatch term "case e return z ⇒ C of { a ⋄ b, ω.ih ⇒ u }"
+      `(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {})
+        (CaseW (PV "a" _) (PV "b" _) (PQ Any _, PV "ih" _) (V "u" {}) _) _),
+    parseMatch term "case e return z ⇒ C of { a ⋄ b, ih ⇒ u }"
+      `(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {})
+        (CaseW (PV "a" _) (PV "b" _) (PQ One _, PV "ih" _) (V "u" {}) _) _),
+    parseMatch term "case e return z ⇒ C of { a ⋄ b ⇒ u }"
+      `(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {})
+        (CaseW (PV "a" _) (PV "b" _) (PQ Zero _, Unused _) (V "u" {}) _) _),
+    parseMatch term "case e return z ⇒ C of { a ⋄ b, _ ⇒ u }"
+      `(Case (PQ One _) (V "e" {}) (PV "z" _, V "C" {})
+        (CaseW (PV "a" _) (PV "b" _) (PQ Zero _, Unused _) (V "u" {}) _) _)
   ],
 
   "definitions" :- [