+simplCast :: SimplEnv -> InExpr -> Coercion -> SimplCont -> SimplM FloatsWithExpr
+simplCast env body co cont
+ = let
+ addCoerce co cont
+ | (s1, k1) <- coercionKind co
+ , s1 `tcEqType` k1 = cont
+ addCoerce co1 (CoerceIt co2 cont)
+ | (s1, k1) <- coercionKind co1
+ , (l1, t1) <- coercionKind co2
+ -- coerce T1 S1 (coerce S1 K1 e)
+ -- ==>
+ -- e, if T1=K1
+ -- coerce T1 K1 e, otherwise
+ --
+ -- For example, in the initial form of a worker
+ -- we may find (coerce T (coerce S (\x.e))) y
+ -- and we'd like it to simplify to e[y/x] in one round
+ -- of simplification
+ , s1 `coreEqType` t1 = cont -- The coerces cancel out
+ | otherwise = CoerceIt (mkTransCoercion co1 co2) cont
+
+ addCoerce co (ApplyTo dup arg arg_se cont)
+ | not (isTypeArg arg) -- This whole case only works for value args
+ -- Could upgrade to have equiv thing for type apps too
+ , Just (s1s2, t1t2) <- splitCoercionKind_maybe co
+ , isFunTy s1s2
+ -- co : s1s2 :=: t1t2
+ -- (coerce (T1->T2) (S1->S2) F) E
+ -- ===>
+ -- coerce T2 S2 (F (coerce S1 T1 E))
+ --
+ -- t1t2 must be a function type, T1->T2, because it's applied
+ -- to something but s1s2 might conceivably not be
+ --
+ -- When we build the ApplyTo we can't mix the out-types
+ -- with the InExpr in the argument, so we simply substitute
+ -- to make it all consistent. It's a bit messy.
+ -- But it isn't a common case.
+ = result
+ where
+ -- we split coercion t1->t2 :=: s1->s2 into t1 :=: s1 and
+ -- t2 :=: s2 with left and right on the curried form:
+ -- (->) t1 t2 :=: (->) s1 s2
+ [co1, co2] = decomposeCo 2 co
+ new_arg = mkCoerce (mkSymCoercion co1) arg'
+ arg' = case arg_se of
+ Nothing -> arg
+ Just arg_se -> substExpr (setInScope arg_se env) arg
+ result = ApplyTo dup new_arg (Just $ zapSubstEnv env)
+ (addCoerce co2 cont)
+ addCoerce co cont = CoerceIt co cont
+ in
+ simplType env co `thenSmpl` \ co' ->
+ simplExprF env body (addCoerce co' cont)
+\end{code}
+
+%************************************************************************
+%* *
+\subsection{Lambdas}
+%* *
+%************************************************************************
+
+\begin{code}