Civilized error messages

I spent the weekend fixing bugs in preparation for the upcoming 0.4 release. I've finished all the necessary compiler hacking, but still need to update the cabal files, tutorial, and wiki before releasing it proper. I've made sure to fix all the bugs that would result in a poor user experience for people that just want to spend an afternoon kicking the tyres. Even though DDC still has lots of missing features (garbage collection, compilation for higher order functions etc), the stuff that is implemented is reasonably well baked. If one tries to do something unsupported it should at least give a civilized error message.

For example:

Trying to use an anonymous type function (higher order functions are not supported yet)

module Test with letrec
  id [a : Data] (x : a) : a  
   = x

  foo (_ : Unit) : Unit
   = do   id (/\a. \(x : a). x)
          ()

Fragment violation when converting Tetra module to Salt module.
  Cannot convert expression.
    Cannot convert type abstraction in this context.
    The program must be lambda-lifted before conversion.
  
    with: /\(a : Data). \(x : a). x

Trying to use higher kinded type arguments (which need an 'Any' region to implement safely, in general)

module Test 
data List (a : Data) where
        Nil  : a -> List a
        Cons : a -> List a -> List a
with letrec
 foo [a : Data ~> Data] [b : Data] (x : b) : b
  = x

 bar (_ : Unit) : Nat#
  = foo [List] [Nat#] 5#
  
Cannot convert expression.
  Unsupported type argument to function or constructor.
  In particular, we don't yet handle higher kinded type arguments.
    
  See [Note: Salt conversion for higher kinded type arguments] in
  the implementation of the Tetra to Salt conversion.
  
  with: [List]

Trying to partially apply a primitive operator:

module Test with letrec
 thing (_ : Unit) : Nat# -> Nat#
  = add# [Nat#] 5#

Fragment violation when converting Tetra module to Salt module.
  Cannot convert expression.
    Partial application of primitive operators is not supported.
  
    with: add# [Nat#] 5#

In contrast, the old ddc-alpha compiler (which I wrote for my PhD work), would signal its displeasure with partially applied primops by producing a program that segfaulted at runtime. We turn our backs on the bad old days.

Nested Data Types

Pleasingly, the new type inferencer does seem to work with some non-standard programs -- even though these don't compile all the way to object code yet. Here is a Core Tetra program using nested data types:

module Test
  data Tuple2 (a b : Data) where
    T2      : a -> b -> Tuple2 a b

  data Nest (a : Data) where
    NilN    : Nest a
    ConsN   : a -> Nest (Tuple2 a a) -> Nest a

with letrec
  thing (_ : Unit)
   = ConsN 7# (ConsN (T2 1# 2#) (ConsN (T2 (T2 6# 7#) (T2 7# 4#)) NilN))

This example is based on one from the Bird and Meertens 1998 paper. Note that the second argument of the ConsN constructor takes a Nest where the element type is more complex than the original parameter. The type inference algorithm in the alpha compiler would have diverged on this program.

Higher Rank Types

I've also tried out some simple examples with higher ranked types, here is one:

module Test with letrec
 thing1 (blerk : ([a : Data]. a -> a) -> Nat#) : Nat#
  = blerk (/\a. \(x : a). x)

 thing2 (u : Unit)
  = thing1 (\(f : [a : Data]. a -> a). f 5#)

thing1 has a rank-3 type because it is a function, that takes a function, that takes a function which is polymorphic. There is a quantifier that appears at depth 3 contravariantly. Writing the type of thing1 in full makes this easier to see:

 thing1 :: ((([a : Data]. a -> a) -> Nat#) -> Nat#

Again, I can't compile this example to object code yet because code generation for higher order functions isn't finished. However, type inference is a separate concern, and I don't know of any remaining problems in this part.