+-- | Returns @Just (dc, [t1..tk], [x1..xn])@ if the argument expression is
+-- a *saturated* constructor application of the form @dc t1..tk x1 .. xn@,
+-- where t1..tk are the *universally-qantified* type args of 'dc'
+exprIsConApp_maybe :: IdUnfoldingFun -> CoreExpr -> Maybe (DataCon, [Type], [CoreExpr])
+
+exprIsConApp_maybe id_unf (Note note expr)
+ | notSccNote note
+ = exprIsConApp_maybe id_unf expr
+ -- We ignore all notes except SCCs. For example,
+ -- case _scc_ "foo" (C a b) of
+ -- C a b -> e
+ -- should not be optimised away, because we'll lose the
+ -- entry count on 'foo'; see Trac #4414
+
+exprIsConApp_maybe id_unf (Cast expr co)
+ = -- Here we do the KPush reduction rule as described in the FC paper
+ -- The transformation applies iff we have
+ -- (C e1 ... en) `cast` co
+ -- where co :: (T t1 .. tn) ~ to_ty
+ -- The left-hand one must be a T, because exprIsConApp returned True
+ -- but the right-hand one might not be. (Though it usually will.)
+
+ case exprIsConApp_maybe id_unf expr of {
+ Nothing -> Nothing ;
+ Just (dc, _dc_univ_args, dc_args) ->
+
+ let (_from_ty, to_ty) = coercionKind co
+ dc_tc = dataConTyCon dc
+ in
+ case splitTyConApp_maybe to_ty of {
+ Nothing -> Nothing ;
+ Just (to_tc, to_tc_arg_tys)
+ | dc_tc /= to_tc -> Nothing
+ -- These two Nothing cases are possible; we might see
+ -- (C x y) `cast` (g :: T a ~ S [a]),
+ -- where S is a type function. In fact, exprIsConApp
+ -- will probably not be called in such circumstances,
+ -- but there't nothing wrong with it
+
+ | otherwise ->
+ let
+ tc_arity = tyConArity dc_tc
+ dc_univ_tyvars = dataConUnivTyVars dc
+ dc_ex_tyvars = dataConExTyVars dc
+ arg_tys = dataConRepArgTys dc
+
+ dc_eqs :: [(Type,Type)] -- All equalities from the DataCon
+ dc_eqs = [(mkTyVarTy tv, ty) | (tv,ty) <- dataConEqSpec dc] ++
+ [getEqPredTys eq_pred | eq_pred <- dataConEqTheta dc]
+
+ (ex_args, rest1) = splitAtList dc_ex_tyvars dc_args
+ (co_args, val_args) = splitAtList dc_eqs rest1
+
+ -- Make the "theta" from Fig 3 of the paper
+ gammas = decomposeCo tc_arity co
+ theta = zipOpenTvSubst (dc_univ_tyvars ++ dc_ex_tyvars)
+ (gammas ++ stripTypeArgs ex_args)
+
+ -- Cast the existential coercion arguments
+ cast_co (ty1, ty2) (Type co)
+ = Type $ mkSymCoercion (substTy theta ty1)
+ `mkTransCoercion` co
+ `mkTransCoercion` (substTy theta ty2)
+ cast_co _ other_arg = pprPanic "cast_co" (ppr other_arg)
+ new_co_args = zipWith cast_co dc_eqs co_args
+
+ -- Cast the value arguments (which include dictionaries)
+ new_val_args = zipWith cast_arg arg_tys val_args
+ cast_arg arg_ty arg = mkCoerce (substTy theta arg_ty) arg
+ in
+#ifdef DEBUG
+ let dump_doc = vcat [ppr dc, ppr dc_univ_tyvars, ppr dc_ex_tyvars,
+ ppr arg_tys, ppr dc_args, ppr _dc_univ_args,
+ ppr ex_args, ppr val_args]
+ in
+ ASSERT2( coreEqType _from_ty (mkTyConApp dc_tc _dc_univ_args), dump_doc )
+ ASSERT2( all isTypeArg (ex_args ++ co_args), dump_doc )
+ ASSERT2( equalLength val_args arg_tys, dump_doc )
+#endif
+
+ Just (dc, to_tc_arg_tys, ex_args ++ new_co_args ++ new_val_args)
+ }}
+
+exprIsConApp_maybe id_unf expr
+ = analyse expr []