- eat_args status metasenv (Inst acc)
- context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl
+ (match classify status ~metasenv context arg with
+ | `PropKind -> assert false (*TODO: same as below, coercion needed???*)
+ | `Proposition
+ | `Term `TypeFormer
+ | `Kind ->
+ eat_args status metasenv (UnsafeCoerce (Inst acc))
+ context (fomega_subst 1 Unit t) tl
+ | `Term _ -> assert false (*TODO: ????*)
+ | `KindOrType
+ | `Type ->
+ eat_args status metasenv (Inst acc)
+ context (fomega_subst 1 (typ_of status ~metasenv context arg) t)
+ tl)