- (co_fn, out_ty) = refineType refinement (idType the_arg_id)
-
- rhs = ASSERT(out_ty `coreEqType` field_tau) perform_co co_fn (Var the_arg_id)
-
- perform_co (ExprCoFn co) expr = Cast expr co
- perform_co id_co expr = ASSERT(isIdCoercion id_co) expr
-
- -- split the uniq_list into two
- uniqs = takeHalf uniq_list
- uniqs' = takeHalf (drop 1 uniq_list)
+ (co_fn, res_ty) = refineType refinement (idType the_arg_id)
+ -- Generate the refinement for b'=b,
+ -- and apply to (Maybe b'), to get (Maybe b)