2009/2/18 Luke Palmer <lrpalmer@gmail.com>:
> ...

> Using dependent types, you could have Prime come with a proof that the
> integer it contains is prime, and thus make those assumptions explicit and
> usable in the implementation. Unfortunately, it would be a major pain in
> the ass to do that in Haskell (for one, your algorithm would have to be
> implemented at the type level with annoying typeclasses to reify number
> types to real integers, and... yeah, people say Haskell has dependent types,
> but not in any reasonable way :-). Dependent languages like Agda, Coq, and
> Epigram are designed for this kind of thing.

I'm curious to know whether a type system exists in which such a
constraint on the type of an argument can be expressed and enforced.

See Agda, Coq, and Epigram.

For example, in Coq, the type of prime numbers is { n : Nat | prime n }, and then when you destruct this, you get an n with the assumption prime n, which can be used in proofs.

In such a case, does the compiler will ever terminate the
type-checking phase?

All three of the above languages are total, in that they may not infinite loop (even at runtime).

Luke