<p dir="ltr">On Nov 15, 2016 12:24 AM, "wren romano" <<a href="mailto:winterkoninkje@gmail.com">winterkoninkje@gmail.com</a>> wrote:<br>
> > subst :: a :~: b -> f a -> f b<br>
> > subst Refl x = x<br>
><br>
> I'm all for adding this function, but do note that the type is<br>
> suboptimal since GHC lacks general functions (and higher-order pattern<br>
> matching) at the type level. Which means we'll actually end up wanting<br>
> a family of different "subst" functions to cover all the (relevant)<br>
> cases the definition above would cover in a language like Agda, Coq,<br>
> etc.</p>
<p dir="ltr">Yes, we will, but those can be written using `subst` and one or more auxiliary types without additional "primitive" eliminators (see below).</p>
<p dir="ltr">> E.g.,<br>
><br>
>     Prelude> let x :: Either Bool Int; x = Right 42<br>
><br>
>     Prelude> :t (`subst` x)<br>
>     (`subst` x) :: Int :~: b -> Either Bool b<br>
><br>
> When I might've really wanted/meant (Bool :~: b -> Either b Int)</p>
<p dir="ltr">We can write</p>
<p dir="ltr">newtype Flip f x y = Flip { unFlip :: f y x }</p>
<p dir="ltr">subst2 :: a :~: b -> f a x -> f b x<br>
subst2 eq = unFlip . subst eq . Flip</p>
<p dir="ltr">The subst2 function will work on the left side of Either.</p>