+ ---------------
+ ok_arg :: Var -- Of type bndr_t
+ -> CoreExpr -- Of type arg_t
+ -> CoercionI -- Of kind (t1~t2)
+ -> Maybe CoercionI -- Of type (arg_t -> t1 ~ bndr_t -> t2)
+ -- (and similarly for tyvars, coercion args)
+ -- See Note [Eta reduction with casted arguments]
+ ok_arg bndr (Type ty) co
+ | Just tv <- getTyVar_maybe ty
+ , bndr == tv = Just (mkForAllTyCoI tv co)
+ ok_arg bndr (Var v) co
+ | bndr == v = Just (mkFunTyCoI (IdCo (idType bndr)) co)
+ ok_arg bndr (Cast (Var v) co_arg) co
+ | bndr == v = Just (mkFunTyCoI (ACo (mkSymCoercion co_arg)) co)
+ -- The simplifier combines multiple casts into one,
+ -- so we can have a simple-minded pattern match here
+ ok_arg _ _ _ = Nothing