| WEBrak : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
| WEEsc : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
| WEBrak : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
| WEEsc : CoreVar -> WeakTypeVar -> WeakExpr -> WeakType -> WeakExpr
| WELetRec rb e => weakTypeOfWeakExpr e
| WENote n e => weakTypeOfWeakExpr e
| WECast e (weakCoercion _ t1 t2 _) => OK t2
| WELetRec rb e => weakTypeOfWeakExpr e
| WENote n e => weakTypeOfWeakExpr e
| WECast e (weakCoercion _ t1 t2 _) => OK t2
(* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
| WEBrak _ ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t')
(* note that we willfully ignore the type stashed in WEBrak/WEEsc here *)
| WEBrak _ ec e _ => weakTypeOfWeakExpr e >>= fun t' => OK (WCodeTy ec t')