So in Idris it's perfectly valid to write the following.
item : (b : Bool) -> if b then Nat else List Nat
item True = 42
item False = [1,2,3] // cf. https://www.youtube.com/watch?v=AWeT_G04a0A
Without the type signature, this looks like a dynamically typed language. But, indeed, Idris is dependently-typed. The concrete type of item b can only be determined during run-time.
This is, of course, a Haskell-programmer talking: The type of item b in the Idris sense is given during compile-time, it is if b then Nat ....
Now my question: Am I right to conclude that in Haskell, the border between the runtime and the compiletime runs exactly between the world of values (False, "foo", 3) and the world of types (Bool, String, Integer) whereas in Idris, the border between the runtime and the compiletime goes across universes?
Also, am I right to assume that even with dependent types in Haskell (using DataKinds and TypeFamilies, cf. this article) the above example is impossible in Haskell, because Haskell contrary to Idris does not allow values to leak to the type-level?
Yes, you're right to observe that the types versus values distinction in Idris does not align with the compiletime-only versus runtime-and-compiletime distinction. That's a good thing. It is useful to have values which exist only at compiletime, just as in program logics we have "ghost variables" used only in specifications. It is useful also to have type representations at runtime, allowing datatype generic programming.
In Haskell, DataKinds (and PolyKinds) let us write
type family Cond (b :: Bool)(t :: k)(e :: k) :: k where
Cond 'True t e = t
Cond 'False t e = e
and in the not too distant future, we shall be able to write
item :: pi (b :: Bool) -> Cond b Int [Int]
item True = 42
item False = [1,2,3]
but until that technology is implemented, we have to make do with singleton forgeries of dependent function types, like this:
data Booly :: Bool -> * where
Truey :: Booly 'True
Falsey :: Booly 'False
item :: forall b. Booly b -> Cond b Int [Int]
item Truey = 42
item Falsey = [1,2,3]
You can get quite far with such fakery, but it would all get a lot easier if we just had the real thing.
Crucially, the plan for Haskell is to maintain and separate forall and pi, supporting parametric and ad hoc polymorphism, respectively. The lambdas and applications that go with forall can still be erased in runtime code generation, just as now, but those for pi are retained. It would also make sense to have runtime type abstractions pi x :: * -> ... and throw the rats' nest of complexity that is Data.Typeable into the dustbin.