[Haskell-cafe] working my way through Data.Type.Equality...my head hurts...

[Jan Stolarek]

> 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/TwoPassMerge/RankProof.hs#L361

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/WhyDependentTypesMatter.hs#L220

HTH

Janek