What does “~” mean…(it’s something that comes out in error messages when my types are all messed up)…. It means GHC knows that two types are equal.
and then there’s a “=>” going on…in the middle of a signature….I know “=>” in the context of “Num a => a -> a -> a” Yeah, that looks scary. You use gcastWith when you need a value of type a but you have a value of type b with a proof that a and b are equal (here a proof is a value of a :~: b). I have a practical example, though perhaps it's not the simplest one:
https://github.com/jstolarek/dep-typed-wbl-heaps-hs/blob/master/src/TwoPassM... This code is thought as an intermediate level tutorial - you might want to give it a try. Another example I have is here (I use the name subst, but it's identical to gcastWith): https://github.com/jstolarek/why-dependent-types-matter/blob/master/WhyDepen... HTH Janek