On Mon, 26 Feb 2007 17:28:59 -0800 (PST) oleg@pobox.com wrote:
The problem with GADTs and other run-time based evidence is just that: _run-time_ based evidence and pattern-matching. In a non-strict system, checking that the evidence is really present is the problem on and of itself.
That's a problem in any system that does not have both termination checking and exhaustive coverage checking. In this presence of both those checks, laziness is not a problem.
BTW, Omega, Dependent ML and a few other systems with GADTs are strict.
Omega does not yet have termination checking AFAIK, and Dependent ML has a more limited type language. Coq does have termination checking, and Neil Mitchell is working on a case-and-termination checker for Haskell. -- Robin