Comment by rtpg

  getValue : (b : Bool) -> pickType b
  getValue True  = 42
  getValue False = "hello"

So given something like this, imagine something like the following:

  someBool = flipACoinToGetABool
  thingy = getValue someBool

You're already in trouble here right? what's the type of thingy?

So maybe you write:

  thingy: (pickType someBool) = getValue someBool

which is fine and great!

then you write:

  print (thingy + 3) -- thingy can be an int right?

But at this point thingy is of type "pickType someBool" while + is expecting Int. So it's up to you to restructure your code to prove to the type checker that someBool is in fact True.

For example:

   print ((if someBool then thingy else 5) + 3)

^ and here your code proves the fact! So in practice when you want to explore the results that are hidden behind the dependent types, you will need to have written code that unwraps it like this. But the whole point is the underpinning type theory means that you will be fine while doing it! You've proven that it'll be fine, so if you add thingy to 3 you'll have an integer.

I think of this stuff a bit like encryption password. You have this bundle of data, but to get in, you need to provide proof that what you're doing won't blow up. You'll need to write your code in a certain way to do it. But if you provide the right proof, then we're golden.