coq typing relation: add DescendImplicit rule in addition to Descend rule for explicit type-downcasts

add one more typing example

coq/typing.v

@@ -64,11 +64,16 @@ Inductive expr_type : context -> expr_term -> type_term -> Prop :=
     (τ' :<= τ) ->
     (Γ |- (expr_ascend τ' e) \is τ')
 
-  | T_Descend : forall Γ x τ τ',
+  | T_DescendImplicit : forall Γ x τ τ',
     Γ |- x \is τ ->
     (τ :<= τ') ->
     Γ |- x \is τ'
 
+  | T_Descend : forall Γ x τ τ',
+    Γ |- x \is τ ->
+    (τ :<= τ') ->
+    Γ |- (expr_descend τ' x) \is τ'
+
 where "Γ '|-' x '\is' τ" := (expr_type Γ x τ).
 
 Definition is_well_typed (e:expr_term) : Prop :=
@@ -92,7 +97,7 @@ Example typing2 :
   ctx_empty |- [{ Λ"T" ↦ λ "x" %"T"% ↦ %"x"% }] \is [< ∀"U", %"U"% -> %"U"% >].
 Proof.
   intros.
-  apply T_Descend with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
+  apply T_DescendImplicit with (τ:=[< ∀"T",(%"T"% -> %"T"%) >]).
   apply T_TypeAbs.
   apply T_Abs.
   apply T_Var.
@@ -114,7 +119,7 @@ Example typing3 :
   >].
 Proof.
   intros.
-  apply T_Descend with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]).
+  apply T_DescendImplicit with (τ:=[< ∀"T",∀"U",(%"T"%->%"U"%->%"U"%) >]) (τ':=[< ∀"S",∀"T",(%"S"%->%"T"%->%"T"%) >]).
   apply T_TypeAbs, T_TypeAbs, T_Abs.
   apply T_Abs.
   apply T_Var.
@@ -153,9 +158,59 @@ Proof.
   apply T_TypeAbs.
   apply T_Abs.
   apply T_Abs.
-  apply C_shuffle. apply C_take.
+  apply T_Var.
+  apply C_shuffle, C_take.
+Qed.
+
+Open Scope ladder_expr_scope.
+
+Example typing5 : (is_well_typed
+  [{
+    let "deg2turns" :=
+       (λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
+                ↦morph (((%"/"% %"x"%) %"360"%) as $"Angle"$~$"Turns"$~$"ℝ"$))
+    in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$~$"ℝ"$) )
+  }]
+).
+Proof.
+  unfold is_well_typed.
+  exists (ctx_assign "60" [< $"ℝ"$ >]
+          (ctx_assign "360" [< $"ℝ"$ >]
+          (ctx_assign "/" [< $"ℝ"$ -> $"ℝ"$ -> $"ℝ"$ >]
+              ctx_empty))).
+  exists [< $"Angle"$~$"Turns"$~$"ℝ"$ >].
+  apply T_Let with (σ:=[< $"Angle"$~$"Degrees"$~$"ℝ"$ ->morph $"Angle"$~$"Turns"$~$"ℝ"$ >]).
+  apply T_MorphAbs.
+  apply T_Ascend with (τ:=[< $"ℝ"$ >]).
+  apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
+  apply T_App with (σ := [< $"ℝ"$ >]) (σ' := [< $"ℝ"$ >]).
+  apply T_Var.
+  apply C_shuffle. apply C_shuffle. apply C_shuffle. apply C_take.
+  apply T_DescendImplicit with (τ := [< $"Angle"$~$"Degrees"$~$"ℝ"$ >]).
   apply T_Var.
   apply C_take.
+  apply TSubRepr_Ladder. apply TSubRepr_Ladder.
+  apply TSubRepr_Refl. apply TEq_Refl.
+  apply M_Sub.
+  apply TSubRepr_Refl. apply TEq_Refl.
+  apply T_Var.
+  apply C_shuffle, C_shuffle, C_take.
+  apply M_Sub.
+  apply TSubRepr_Refl.
+  apply TEq_Refl.
+  apply TSubRepr_Ladder, TSubRepr_Ladder, TSubRepr_Refl.
+  apply TEq_Refl.
+  apply T_App with (σ:=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]) (σ':=[<$"Angle"$~$"Degrees"$~$"ℝ"$>]).
+  apply T_MorphFun.
+  apply T_Var.
+  apply C_take.
+  apply T_Ascend with (τ:=[<$"ℝ"$>]).
+  apply T_Var.
+  apply C_shuffle. apply C_take.
+  apply TSubRepr_Ladder.
+  apply TSubRepr_Ladder.
+  apply TSubRepr_Refl. apply TEq_Refl.
+  apply M_Sub. apply TSubRepr_Refl. apply TEq_Refl.
 Qed.
 
 End Typing.