Need support of error to represent unrecoverable logical error

[zonyitoo]

We probably need support of error just like the one in Haskell. It won't be able to write one by user, because that will cause a type mismatch error.

Example use case:

let car [A] (l : PolyList[A]) : A =
    case l of
        Nil         -> error "Call `car` on a empty list"
     |  Cons x xs   -> x;

If I define error like this

let error (msg : String) = {
    java.lang.System.err.println(msg);
    java.lang.System.exit(1);
    ()
};

It won't compile, because of type mismatch. So I think compiler should see error function as a special case, or provide mechanisms to support throwing exception.

In Haskell, the message that sent from error function could be caught by Control.Exception.catch.

The definition of error in Haskell is

error :: [Char] -> a

[zonyitoo]

Moreover, if I define error like this

let error [A] (msg : String) : A = {
    java.lang.System.err.println(msg);
    java.lang.System.exit(1);

    -- What should I write here??
};

[brunocdsoliveira]

Perhaps we need an easy way to add primitives into the compiler, including error and tracing features. Maybe @bixuanzju can think a bit about this.